proposition: Lemma zring_old_diff : forall m n : nat, zring_old (m - n) [=] nring m[-]nring n.
proof: Proof. unfold zring_old in |- *. intros m n. apply proper_caseZ_diff_CS with (f := fun m0 n0 : nat => nring (R:=R) m0[-]nring n0). clear m n. intros m n p q H. apply cg_cancel_lft with (nring n:R). unfold cg_minus in |- *. astepl (nring (R:=R) n[+] ( [--] (nring n) [+]nring m)). astepl (nring (R:=R) n[+] [--] (nring n) [+]nring m). astepl ([0][+]nring (R:=R) m). astepl (nring (R:=R) m). apply cg_cancel_rht with (nring q:R). astepr (nring (R:=R) n[+] (nring p[+] [--] (nring q) [+]nring q)). astepr (nring (R:=R) n[+] (nring p[+] ( [--] (nring q) [+]nring q))). astepr (nring (R:=R) n[+] (nring p[+][0])). astepr (nring (R:=R) n[+]nring p). astepr (nring (R:=R) (n + p)). astepl (nring (R:=R) (m + q)). rewrite H. algebra. 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)