chore(data/nat/cast,algebra/ordered_group): 2 trivial lemmas (#5436)

Author: urkud

src/algebra/ordered_group.lean

@@ -325,6 +325,10 @@ lemma lt_inv' : a < b⁻¹ ↔ b < a⁻¹ :=
 have (a⁻¹)⁻¹ < b⁻¹ ↔ b < a⁻¹, from inv_lt_inv_iff,
 by rwa inv_inv at this
 
+@[to_additive]
+lemma inv_lt_self (h : 1 < a) : a⁻¹ < a :=
+(inv_lt_one'.2 h).trans h
+
 @[to_additive]
 lemma le_inv_mul_iff_mul_le : b ≤ a⁻¹ * c ↔ a * b ≤ c :=
 have a⁻¹ * (a * b) ≤ a⁻¹ * c ↔ a * b ≤ c, from mul_le_mul_iff_left _,

src/data/nat/cast.lean

@@ -270,6 +270,10 @@ begin
   exact with_top.coe_le_coe.2 (with_top.coe_lt_coe.1 h)
 end
 
+lemma one_le_iff_pos {n : with_top ℕ} : 1 ≤ n ↔ 0 < n :=
+⟨λ h, (coe_lt_coe.2 zero_lt_one).trans_le h,
+  λ h, by simpa only [zero_add] using add_one_le_of_lt h⟩
+
 @[elab_as_eliminator]
 lemma nat_induction {P : with_top ℕ → Prop} (a : with_top ℕ)
   (h0 : P 0) (hsuc : ∀n:ℕ, P n → P n.succ) (htop : (∀n : ℕ, P n) → P ⊤) : P a :=