proposition: Lemma zring_old_inv : forall i, zring_old (- i) [=] [--] (zring_old i).
proof: Proof. intro i. pattern i in |- *. apply diff_Z_ind. intros m n. replace (- (m - n))%Z with (n - m)%Z. astepl (nring (R:=R) n[-]nring m). astepr ( [--] (nring (R:=R) m[-]nring n)). unfold cg_minus in |- *. astepr ( [--] (nring m) [+] [--][--] (nring (R:=R) n)). Step_final ( [--] (nring (R:=R) m) [+]nring n). 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)