proposition: Lemma zring_old_plus : forall i j, zring_old (i + j) [=] zring_old i[+]zring_old j.
proof: Proof. intros i j. pattern i in |- *. apply diff_Z_ind. intros m n. pattern j in |- *. apply diff_Z_ind. intros m0 n0. Hint Resolve zring_old_diff: algebra. replace (m - n + (m0 - n0))%Z with ((m + m0)%nat - (n + n0)%nat)%Z. astepl (nring (m + m0) [-]nring (n + n0):R). astepl (nring m[+]nring m0[-] (nring n[+]nring n0):R). astepr (nring m[-]nring n[+] (nring m0[-]nring n0):R). unfold cg_minus in |- *. astepl (nring m[+] (nring m0[+] [--] (nring n[+]nring n0)):R). astepr (nring m[+] ( [--] (nring n) [+] (nring m0[+] [--] (nring n0))):R). apply bin_op_wd_unfolded. algebra. astepl (nring m0[+] ( [--] (nring n) [+] [--] (nring n0)):R). astepl (nring m0[+] [--] (nring n) [+] [--] (nring n0):R). Step_final ( [--] (nring n) [+]nring m0[+] [--] (nring n0):R). repeat rewrite Znat.inj_plus. auto with zarith. 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)