proposition: Lemma divq_num_den x : (numq x)%:Q / (denq x)%:Q = x.
proof: Proof. by rewrite -{3}[x]valqK [valq _]surjective_pairing /= fracqE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)