proposition: Fact ratz_frac n : ratz n = fracq (n, 1).
proof: Proof. by apply: val_inj; rewrite val_fracq/= gcdn1 !divn1 abszE mulr_sign_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)