proposition: Lemma iso_is_rationals: Rationals F.
proof: Proof. repeat (split; unfold rationals_to_frac; try apply _). intros x y E. apply (injective (f ∘ integers_to_ring Z Q)). now rewrite 2!(to_ring_unique (f ∘ integers_to_ring Z Q)). 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