proposition: Lemma nexp_mult : forall (x : R) m n, (x[^]m) [^]n [=] x[^] (m * n).
proof: Proof. intros x m n. induction m as [| m Hrecm]. simpl in |- *. Step_final (([1]:R) [^]n). astepl ((x[*]x[^]m) [^]n). astepl (x[^]n[*] (x[^]m) [^]n). astepl (x[^]n[*]x[^] (m * n)). astepl (x[^] (n + m * n)). replace (n + m * n) with (S m * n); algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)