proposition: Lemma morphisms_involutive `{Integers Z} `{Integers Z2} (f: Z → Z2) (g: Z2 → Z) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x : f (g x) = x.
proof: Proof. now apply (to_ring_unique_alt (f ∘ g) id). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.implementations.natpair_integers MathClasses.interfaces.integers