proposition: Lemma rationals_decompose `{!SemiRing_Morphism (f : Z → Q)} (x : Q) : ∃ num, ∃ den, den ≠ 0 ∧ x = f num / f den.
proof: Proof. exists (num (QtoFrac x)), (den (QtoFrac x)). split. now apply den_ne_0. apply (injective QtoFrac). rewrite preserves_mult. rewrite preserves_dec_recip. change (QtoFrac x = (QtoFrac ∘ f) (num (QtoFrac x)) / (QtoFrac ∘ f) (den (QtoFrac x))). rewrite 2!(to_ring_unique_alt (QtoFrac ∘ f) Frac_inject). assert (Frac_inject (den (QtoFrac x)) ≠ 0) as P. apply injective_ne_0. apply den_ne_0. apply Frac_dec_mult_num_den. 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