proposition: Lemma inject_bigQ_frac_bigZ_correct: cast bigQ (Frac bigZ) = rationals_to_frac bigQ bigZ.
proof: Proof. intros x y E. rewrite <-E. clear y E. destruct x as [n|n d]. rapply (integers.to_ring_unique_alt (cast bigZ (Frac bigZ)) (rationals_to_frac bigQ bigZ ∘ cast bigZ bigQ)). unfold cast at 1. simpl. rewrite bigQ_div_bigQq_alt. rewrite rings.preserves_mult, dec_fields.preserves_dec_recip. case (decide_rel (=) ('d : bigZ) 0); intros Ed. rewrite Ed. rewrite !rings.preserves_0. rewrite dec_recip_0. now rewrite rings.mult_0_r. rewrite 2!(integers.to_ring_twice _ _ (cast bigZ (Frac bigZ))). now rewrite Frac_dec_mult_num_den at 1. Qed.
imports: Coq.QArith.QArith Bignums.BigQ.BigQ MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations MathClasses.implementations.fast_naturals MathClasses.implementations.fast_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.stdlib_rationals MathClasses.implementations.QType_rationals