proposition: Lemma mult_nexp : forall (x y : R) n, (x[*]y) [^]n [=] x[^]n[*]y[^]n.
proof: Proof. intros x y n. induction n as [| n Hrecn]. astepl ([1]:R). Step_final (([1]:R) [*][1]). astepl (x[*]y[*] (x[*]y) [^]n). astepl (x[*]y[*] (x[^]n[*]y[^]n)). astepl (x[*] (y[*] (x[^]n[*]y[^]n))). astepl (x[*] (y[*]x[^]n[*]y[^]n)). astepl (x[*] (x[^]n[*]y[*]y[^]n)). astepl (x[*] (x[^]n[*] (y[*]y[^]n))). Step_final (x[*]x[^]n[*] (y[*]y[^]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)