proposition: Fact fracq_eq x y : x.2 != 0 -> y.2 != 0 -> (fracq x == fracq y) = (x.1 * y.2 == y.1 * x.2).
proof: Proof. case: fracqP=> //= u fx u_neq0 _; case: fracqP=> //= v fy v_neq0 _; symmetry. rewrite [eqbRHS]mulrC mulrACA [eqbRHS]mulrACA. by rewrite [denq _ * _]mulrC (inj_eq (mulfI _)) ?mulf_neq0 // rat_eq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)