proposition: Lemma RatioP n d : Ratio_spec n d (Ratio n d) n d.
proof: Proof. rewrite /Ratio /insubd; case: insubP=> /= [x /= d_neq0 hx|]. have ->: x = @mkRatio (n, d) d_neq0 by apply: val_inj. by constructor. by rewrite negbK=> /eqP hx; rewrite {2}hx; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssrAC choice tuple bigop ssralg poly polydiv) mathcomp(generic_quotient)