Commit 2025-04-15 14:18 cd81a4df
View on Github →chore: exchange Nat.sub_lt_iff_lt_add and Nat.sub_lt_iff_lt_add' (#24080)
This PR swaps Nat.sub_lt_iff_lt_add and Nat.sub_lt_iff_lt_add' to align them with the top-level sub_lt_iff_lt_add and sub_lt_iff_lt_add' lemmas.
leanprover/lean4#7971 will upstream these lemmas with this swapped meaning.