proposition: Fact ge_rat0_norm x : le_rat 0 x -> normq x = x.
proof: Proof. rewrite ge_rat0; case: ratP=> [] // n d cnd n_ge0. by rewrite normqE /= normr_num_div ?ger0_norm // divq_num_den. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)