fact: Definition zring (z : Z) : R := match z with | Z0 => [0] | Zpos p => pring p | Zneg p => [--] (pring p) end.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)