proposition: Lemma Z2int_Qred n d : ((Z2int (Qnum (Qred (n # d))))%:Q / (nat_of_pos (Qden (Qred (n # d))))%:Q = (Z2int n)%:Q / (Z2int (Z.pos d))%:Q)%R.
proof: Proof. rewrite -(fracqE (Z2int n, Z2int (Z.pos d))) -[RHS]divq_num_den. rewrite /Qred. move: (Z.ggcd_gcd n (Z.pos d)) (Z.ggcd_correct_divisors n (Z.pos d)). move: (Z_ggcd_coprime n (Z.pos d)). case: Z.ggcd => g [n' d'] /=. case: g => [|g|g]. { by move=> _ _ [_]; rewrite Z.mul_0_l. } { move=> coprime_n'_d' => _ [->]. rewrite (nat_of_pos_Z_to_pos d) => /[dup] posd' ->. have d'n0 : `|Z2int d'| != 0%R. { rewrite normr_eq0. case: d' posd' {coprime_n'_d'} => // d' _. by rewrite Posz_nat_of_pos_neq0. } rewrite !Z2int_mul abszM PoszM gez0_abs; [|by rewrite -[0%R]int2ZK Z2int_le]. rewrite fracqMM ?Posz_nat_of_pos_neq0 // abszE. move: (@valq_frac (Z2int n', `|Z2int d'|) d'n0). rewrite scalqE // mul1r => [[neq deq]]. have -> : nat_of_pos (Z.to_pos d') = `|Z2int d'| :> int. { rewrite nat_of_pos_Z_to_pos Z2Pos.id ?abszE //. by case: d' posd' {coprime_n'_d' d'n0 neq deq}. } rewrite [X in (X%:~R / _)%R]neq [X in (_ / X%:~R)%R]deq. rewrite (_ : gcdn _ _ = 1%nat) ?mul1r //; exact/eqP/coprime_n'_d'. } by move: (Z.gcd_nonneg n (Z.pos d)) => + _ => /[swap] <-. 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)