proposition: Lemma bigQ_div_bigQq (n : bigZ) (d : bigN) : BigQ.Qq n d = 'n / 'd.
proof: Proof. change (n # d == 'n / (BigQ.Qz (BigZ.Pos d)))%bigQ. unfold BigQ.div, BigQ.inv. case_eq (BigZ.zero ?= BigZ.Pos d)%bigZ; intros Ed. transitivity BigQ.zero; [| ring]. do 2 red. simpl. case_eq (BigN.eqb d BigN.zero); intros Ed2; [reflexivity |]. rewrite BigZ.spec_compare in Ed. destruct (proj2 (not_true_iff_false _) Ed2). apply BigN.eqb_eq. symmetry. now apply Zcompare_Eq_eq. unfold BigQ.mul. simpl. rewrite right_identity. reflexivity. destruct (BigZ.compare_spec BigZ.zero (BigZ.Pos d)); try discriminate. destruct (orders.lt_not_le_flip 0 ('d : bigZ)); trivial. now apply nat_int.to_semiring_nonneg. 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