proposition: Fact fracqMM x n d : x != 0 -> fracq (x * n, x * d) = fracq (n, d).
proof: Proof. move=> x_neq0; apply/eqP. have [->|d_neq0] := eqVneq d 0; first by rewrite mulr0 !fracq0. by rewrite fracq_eq ?mulf_neq0 //= mulrCA mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)