proposition: Lemma divq_eq_deprecated (nx dx ny dy : rat) : dx != 0 -> dy != 0 -> (nx / dx == ny / dy) = (nx * dy == ny * dx).
proof: Proof. exact: eqr_div. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)