proposition: Lemma int_pow_S_nonneg `{Apart B} `{!TrivialApart B} `{!FullPseudoSemiRingOrder (A:=B) Ble Blt} (x : A) (n : B) : 0 ≤ n → x ^ (1+n) = x * x ^ n.
proof: Proof. intros En. destruct (decide (x = 0)) as [Ex | Ex]. rewrite Ex. rewrite int_pow_base_0. ring. intros E. destruct semirings.not_le_1_0. rewrite <-E. now apply semirings.nonneg_plus_le_compat_r. now rewrite int_pow_S. 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