proposition: Fact fracqP x : fracq_spec x x (fracq x).
proof: Proof. case: x => n d /=; have [d_eq0 | d_neq0] := eqVneq d 0. by rewrite d_eq0 fracq0; constructor. by rewrite {2}[(_, _)]valq_frac //; constructor; rewrite scalq_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)