proposition: Fact valq_frac x : x.2 != 0 -> x = (scalq x * numq (fracq x), scalq x * denq (fracq x)).
proof: Proof. move=> x2_neq0; rewrite scalqE//; move: x2_neq0. case: x => [n d] /= d_neq0; rewrite num_fracq den_fracq/= ?d_neq0. rewrite mulr_signM -mulrA -!PoszM addKb. do 2!rewrite muln_divCA ?(dvdn_gcdl, dvdn_gcdr) // divnn. by rewrite gcdn_gt0 !absz_gt0 d_neq0 orbT !muln1 !mulz_sign_abs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)