proposition: Lemma morphisms_involutive `{Rationals Q1} `{Rationals Q2} (f : Q1 → Q2) (g : Q2 → Q1) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} : ∀ x, f (g x) = x.
proof: Proof. intros x. rewrite (to_rationals_unique f), (to_rationals_unique g). apply to_rationals_involutive. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.implementations.field_of_fractions MathClasses.implementations.natpair_integers MathClasses.theory.rings MathClasses.theory.integers MathClasses.theory.dec_fields