proposition: Lemma to_rationals_unique (f : Q1 → Q2) `{!SemiRing_Morphism f} : ∀ x, f x = rationals_to_rationals Q1 Q2 x.
proof: Proof. intros x. apply (injective (rationals_to_rationals Q2 Q1)). rewrite to_rationals_involutive. change ((rationals_to_frac Q1 (SRpair nat)⁻¹) ((rationals_to_frac Q2 (SRpair nat) ∘ f) x) = x). rewrite (to_frac_unique (rationals_to_frac Q2 (SRpair nat) ∘ f) (rationals_to_frac Q1 (SRpair nat))). apply (jections.bijective_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