proposition: Lemma rat_eq x y : (x == y) = (numq x * denq y == numq y * denq x).
proof: Proof. symmetry; rewrite rat_eqE andbC. have [->|] /= := eqVneq (denq _); first by rewrite (inj_eq (mulIf _)). apply: contraNF => /eqP hxy; rewrite -absz_denq -[eqbRHS]absz_denq. rewrite eqz_nat /= eqn_dvd. rewrite -(@Gauss_dvdr _ `|numq x|) 1?coprime_sym ?coprime_num_den // andbC. rewrite -(@Gauss_dvdr _ `|numq y|) 1?coprime_sym ?coprime_num_den //. by rewrite -!abszM hxy -{1}hxy !abszM !dvdn_mull ?dvdnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)