proposition: Lemma r_ratBigQ_red x y : r_ratBigQ x y -> match BigQ.red y with | BigQ.Qz n => numq x = Z2int (BigZ.to_Z n) /\ denq x = 1%R | BigQ.Qq n d => numq x = Z2int (BigZ.to_Z n) /\ denq x = Z2int (BigN.to_Z d) end.
proof: Proof. case: (ratP x) => nx dx nx_dx_coprime {x}. rewrite /r_ratBigQ /fun_hrel unlock -BigQ.strong_spec_red. have ry_red : Qred (BigQ.to_Q (BigQ.red y)) = BigQ.to_Q (BigQ.red y). { by rewrite BigQ.strong_spec_red Qcanon.Qred_involutive. } have ry_dneq0 := BigQ_red_den_nonzero y. case: (BigQ.red y) ry_dneq0 ry_red => [ny _ _|ny dy dy_neq0]. { rewrite /BigQ.to_Q /Qnum /Qden mulr1. move=> /(f_equal ( *%R^~ dx.+1%:~R)%R). rewrite mulfVK ?mulrz_neq0 // -intrM => /intr_inj nx_eq. have dx_1 : (dx.+1 = 1)%nat. { by move: nx_dx_coprime => /eqP <-; rewrite -nx_eq abszM /= gcdnC gcdnMl. } by rewrite -nx_eq dx_1 mulr1. } rewrite /BigQ.to_Q ifF ?BigN.spec_eqb ?Z.eqb_neq //. rewrite Qcanon.Qred_iff ZgcdE -[1%coqZ]/(Z.of_nat 1%nat) => /Nat2Z.inj. rewrite /Qnum /Qden nat_of_pos_Z_to_pos => /eqP ny_dy_coprime. move=> /eqP; rewrite rat_eqE !coprimeq_num // !coprimeq_den //=. rewrite !gtr0_sg ?nat_of_pos_gtr0 // !mul1r => /andP[/eqP <-]. rewrite ifF; [|exact/eqP/eqP/lt0r_neq0/nat_of_pos_gtr0]. rewrite -!abszE !absz_nat => /eqP[<-]; split=> [//|]. rewrite -[LHS]/(Z2int (Z.pos (Z.to_pos (BigN.to_Z dy)))) Z2Pos.id //. exact: BigQ.N_to_Z_pos. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)