fact: Record is_CRing (G : CAbGroup) (One : G) (mult : CSetoid_bin_op G) : CProp := {ax_mult_assoc : associative mult; ax_mult_mon : is_CMonoid (Build_CSemiGroup G mult ax_mult_assoc) One; ax_mult_com : commutes mult; ax_dist : distributive mult csg_op; ax_non_triv : One [#] [0]}.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)