proposition: Lemma tofrac_eq (p q : R): (p%:F == q%:F) = (p == q).
proof: Proof. apply/eqP/eqP=> [|->//]; unlock tofrac=> /eqmodP /eqP /=. by rewrite !numden_Ratio ?(oner_eq0, mul1r, mulr1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)