proposition: Lemma divqP n d : divq_spec n d n d (n%:Q / d%:Q).
proof: Proof. set x := (n, d); rewrite -[n]/x.1 -[d]/x.2 -fracqE. by case: fracqP => [_|k fx k_neq0] /=; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)