proposition: Lemma int_pow_gt_1 (x : A) (n : B) : 1 < x → 0 < n → 1 < x ^ n.
proof: Proof. intros Ex En. apply nat_int.lt_iff_S_le in En. destruct (semirings.decompose_le En) as [z [Ez1 Ez2]]. ring_simplify in Ez2. rewrite Ez2. clear En Ez2 n. revert z Ez1. apply integers.induction_nonneg; try assumption. solve_proper. now rewrite left_identity, right_identity. intros n En E2. rewrite <-associativity, int_pow_S. apply semirings.gt_1_mult_lt_compat_l; auto. transitivity (1:A); [apply semirings.lt_0_1 | assumption]. apply orders.lt_ne_flip. apply orders.le_lt_trans with 1; trivial. now apply semirings.le_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