proposition: Lemma int_pow_exp_plus (n m : B) (x : A) : x ≠ 0 → x ^ (n + m) = x ^ n * x ^ m.
proof: Proof. intros nonneg. revert n. apply biinduction. solve_proper. rewrite int_pow_0, left_identity. ring. intros n. rewrite <-associativity, 2!int_pow_S; trivial. split; intros E. rewrite E. ring. apply (rings.left_cancellation_ne_0 (.*.) x); trivial. rewrite E. ring. 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