proposition: Lemma cring_catamorphism_fun_negate {R} x : cring_catamorphism_fun R (- x) = - cring_catamorphism_fun R x.
proof: Proof. snrapply (groups.preserves_negate _). 1-6: typeclasses eauto. snrapply Build_IsMonoidPreserving. 1: exact _. split. Defined.
imports: Classes.interfaces.abstract_algebra Algebra.AbGroups Algebra.Rings.CRing Spaces.Int Spaces.Pos WildCat.Core