feat(algebra/parity): more general odd.pos (#15186)

The old version of this lemma (added in #13040) was only for ℕ and didn't allow dot notation. We remove this and add a version for `canonically_ordered_comm_semiring`s, and if the definition of `odd` changes, this will also work for `canononically_ordered_add_monoid`s.



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author: ericrbg

archive/imo/imo1998_q2.lean

@@ -201,7 +201,7 @@ theorem imo1998_q2 [fintype J] [fintype C]
   (hk : ∀ (p : judge_pair J), p.distinct → (agreed_contestants r p).card ≤ k) :
   (b - 1) / (2 * b) ≤ k / a :=
 begin
-  rw clear_denominators ha (nat.pos_of_odd hb),
+  rw clear_denominators ha hb.pos,
   obtain ⟨z, hz⟩ := hb, rw hz at hJ, rw hz,
   have h := le_trans (A_card_lower_bound r hJ) (A_card_upper_bound r hk),
   rw [hC, hJ] at h,

src/algebra/parity.lean

@@ -241,6 +241,21 @@ lemma odd.neg_one_pow (h : odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_pow, one_
 
 end monoid
 
+section canonically_ordered_comm_semiring
+
+variables [canonically_ordered_comm_semiring α]
+
+-- this holds more generally in a `canonically_ordered_add_monoid` if we refactor `odd` to use
+-- either `2 • t` or `t + t` instead of `2 * t`.
+lemma odd.pos [nontrivial α] {n : α} (hn : odd n) : 0 < n :=
+begin
+  obtain ⟨k, rfl⟩ := hn,
+  rw [pos_iff_ne_zero, ne.def, add_eq_zero_iff, not_and'],
+  exact λ h, (one_ne_zero h).elim
+end
+
+end canonically_ordered_comm_semiring
+
 section ring
 variables [ring α] {a b : α} {n : ℕ}
 

src/data/nat/parity.lean

@@ -72,9 +72,6 @@ begin
               one_ne_zero, and_self] },
 end
 
-lemma pos_of_odd (h : odd n) : 0 < n :=
-by { obtain ⟨k, rfl⟩ := h, exact succ_pos' }
-
 @[simp] theorem two_dvd_ne_zero : ¬ 2 ∣ n ↔ n % 2 = 1 :=
 even_iff_two_dvd.symm.not.trans not_even_iff