proposition: Fact valqK x : fracq (valq x) = x.
proof: Proof. move: x => [[n d] /= Pnd]; apply: val_inj; rewrite ?val_fracq/=. move: Pnd; rewrite /coprime /fracq /= => /andP[] hd -/eqP hnd. by rewrite lt_gtF ?gt_eqF //= hnd !divn1 mulz_sign_abs abszE gtr0_norm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)