feat(data/{int, nat}/parity): rename ne_of_odd_sum (#7261)

`ne_of_odd_sum` becomes `ne_of_odd_add`.

Author: benjamindavidson

archive/imo/imo1998_q2.lean

@@ -142,7 +142,7 @@ begin
   have h' : (x + y) * (x + y) = 4*z*z + 4*z + 1, { rw h, ring, },
   rw [← add_sq_add_sq_sub, h', add_le_add_iff_left],
   suffices : 0 < (x - y) * (x - y), { apply int.add_one_le_of_lt this, },
-  apply mul_self_pos, rw sub_ne_zero, apply int.ne_of_odd_sum ⟨z, h⟩,
+  apply mul_self_pos, rw sub_ne_zero, apply int.ne_of_odd_add ⟨z, h⟩,
 end
 
 section

src/data/int/parity.lean

@@ -181,7 +181,7 @@ by rw [add_comm, odd_add]
 theorem even.add_odd (hm : even m) (hn : odd n) : odd (m + n) :=
 odd_add'.2 $ iff_of_true hn hm
 
-lemma ne_of_odd_sum (h : odd (m + n)) : m ≠ n :=
+lemma ne_of_odd_add (h : odd (m + n)) : m ≠ n :=
 λ hnot, by simpa [hnot] with parity_simps using h
 
 @[parity_simps] theorem odd_sub : odd (m - n) ↔ (odd m ↔ even n) :=

src/data/nat/parity.lean

@@ -190,7 +190,7 @@ by rw [add_comm, odd_add]
 theorem even.add_odd (hm : even m) (hn : odd n) : odd (m + n) :=
 odd_add'.2 $ iff_of_true hn hm
 
-lemma ne_of_odd_sum (h : odd (m + n)) : m ≠ n :=
+lemma ne_of_odd_add (h : odd (m + n)) : m ≠ n :=
 λ hnot, by simpa [hnot] with parity_simps using h
 
 @[parity_simps] theorem odd_sub (h : n ≤ m) : odd (m - n) ↔ (odd m ↔ even n) :=