proposition: Fact fracq_subproof x (y := fracq_opt_subdef x) : (0 < y.2) && (coprime `|y.1| `|y.2|).
proof: Proof. rewrite {}/y fracq_opt_subdefE /=; have [] //= := eqVneq x.2 0. case: x => [/= n d]; rewrite -absz_gt0 => dN0. have ggt0 : (0 < gcdn `|n| `|d|)%N by rewrite gcdn_gt0 dN0 orbT. rewrite ltz_nat divn_gt0// dvdn_leq ?dvdn_gcdr//=. rewrite abszM abszX abszN1 exp1n mul1n absz_nat. rewrite /coprime -(@eqn_pmul2r (gcdn `|n| `|d|))// mul1n. by rewrite muln_gcdl !divnK ?(dvdn_gcdl, dvdn_gcdr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)