proposition: Lemma to_frac_unique `{Rationals Q} `{Integers Z} (f g : Q → Frac Z) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} : ∀ x, f x = g x.
proof: Proof. intros x. apply (injective (g⁻¹)). change (f⁻¹ (f ⁻¹ ⁻¹ x) = g⁻¹ (g⁻¹ ⁻¹ x)). now rewrite 2!(jections.surjective_applied _). 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