proposition: Lemma rat_eqE x y : (x == y) = (numq x == numq y) && (denq x == denq y).
proof: Proof. rewrite -val_eqE [val x]surjective_pairing [val y]surjective_pairing /=. by rewrite xpair_eqE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)