proposition: Fact mulq_frac x y : (mulq (fracq x) (fracq y)) = fracq (mulq_subdef x y).
proof: Proof. rewrite mulq_def !mulq_subdefE; case: (fracqP x) => /= [|u fx u_neq0]. by rewrite !mul0r !mul1r fracq0 frac0q. case: (fracqP y) => /= [|v fy v_neq0]. by rewrite !mulr0 !mulr1 fracq0 frac0q. by rewrite ![_ * (v * _)]mulrACA fracqMM ?mulf_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)