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