proposition: Lemma zring_old_mult : 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. astepr ((nring (R:=R) m[-]nring n) [*] (nring m0[-]nring n0)). replace ((m - n) * (m0 - n0))%Z with ((m * m0 + n * n0)%nat - (n * m0 + m * n0)%nat)%Z. 2: repeat rewrite Znat.inj_plus. 2: repeat rewrite Znat.inj_mult. 2: repeat rewrite BinInt.Zmult_minus_distr_r. 2: repeat rewrite CornBasics.Zmult_minus_distr_r. 2: auto with zarith. astepl (nring (R:=R) (m * m0 + n * n0) [-]nring (n * m0 + m * n0)). astepl (nring (R:=R) (m * m0) [+]nring (n * n0) [-] (nring (n * m0) [+]nring (m * n0))). astepl (nring (R:=R) m[*]nring m0[+]nring n[*]nring n0[-] (nring n[*]nring m0[+]nring m[*]nring n0)). astepr (nring (R:=R) m[*] (nring m0[-]nring n0) [-]nring n[*] (nring m0[-]nring n0)). astepr (nring (R:=R) m[*]nring m0[-]nring m[*]nring n0[-] (nring n[*]nring m0[-]nring n[*]nring n0)). unfold cg_minus in |- *. astepr (nring (R:=R) m[*]nring m0[+] ( [--] (nring m[*]nring n0) [+] [--] (nring n[*]nring m0[+] [--] (nring n[*]nring n0)))). astepl (nring (R:=R) m[*]nring m0[+] (nring n[*]nring n0[+] [--] (nring n[*]nring m0[+]nring m[*]nring n0))). apply bin_op_wd_unfolded. algebra. astepl (nring (R:=R) n[*]nring n0[+] ( [--] (nring n[*]nring m0) [+] [--] (nring m[*]nring n0))). astepr ( [--] (nring (R:=R) m[*]nring n0) [+] ( [--] (nring n[*]nring m0) [+] [--][--] (nring n[*]nring n0))). astepr ( [--] (nring (R:=R) m[*]nring n0) [+] ( [--] (nring n[*]nring m0) [+]nring n[*]nring n0)). astepr ( [--] (nring (R:=R) m[*]nring n0) [+] (nring n[*]nring n0[+] [--] (nring n[*]nring m0))). astepr ( [--] (nring (R:=R) m[*]nring n0) [+]nring n[*]nring n0[+] [--] (nring n[*]nring m0)). astepr (nring (R:=R) n[*]nring n0[+] [--] (nring m[*]nring n0) [+] [--] (nring n[*]nring m0)). Step_final (nring (R:=R) n[*]nring n0[+] ( [--] (nring m[*]nring n0) [+] [--] (nring n[*]nring m0))). 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)