proposition: Lemma int_pow_ge_1 (x : A) (n : B) : 1 ≤ x → 0 ≤ n → 1 ≤ x ^ n.
proof: Proof. intros E1 E2. revert n E2. apply integers.induction_nonneg; trivial. solve_proper. now rewrite int_pow_0. intros. rewrite int_pow_S. rewrite <-rings.mult_1_r. apply semirings.mult_le_compat; try apply semirings.le_0_1; auto. apply orders.lt_ne_flip. apply orders.lt_le_trans with 1; trivial. now apply semirings.lt_0_1. Qed.
imports: Coq.setoid_ring.Ring Coq.setoid_ring.Field MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.theory.nat_pow MathClasses.theory.int_abs MathClasses.theory.dec_fields