proposition: Lemma nring_comm_mult : forall n m, nring (n * m) [=] nring n[*]nring m.
proof: Proof. intros n m; induction n as [| n Hrecn]; simpl in |- *. algebra. apply eq_transitive_unfolded with (nring m[+]nring (n * m)). apply (nring_comm_plus m (n * m)). astepr (nring n[*]nring m[+][1][*]nring m). astepr (nring n[*]nring m[+]nring m). Step_final (nring m[+]nring n[*]nring m). 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)