proposition: Lemma nexp_plus : forall (x : R) m n, x[^]m[*]x[^]n [=] x[^] (m + n).
proof: Proof. intros x m n. induction m as [| m Hrecm]. rewrite plus_O_n. Step_final ([1][*]x[^]n). rewrite plus_Sn_m. astepl (x[^]m[*]x[*]x[^]n). astepl (x[*]x[^]m[*]x[^]n). astepl (x[*] (x[^]m[*]x[^]n)). Step_final (x[*]x[^] (m + n)). 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)