proposition: Lemma nat_pow_ge_1 (x : A) (n : B) : 1 ≤ x → 1 ≤ x ^ n.
proof: Proof. intros. pattern n. apply naturals.induction. solve_proper. now rewrite nat_pow_0. intros. rewrite nat_pow_S. now apply semirings.ge_1_mult_compat. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations