proposition: Lemma normr_num_div n d : `|numq (n%:~R / d%:~R)| = numq (`|n|%:~R / `|d|%:~R).
proof: Proof. rewrite (normrEsg n) (normrEsg d) !rmorphM /= invfM mulrACA !sgr_def. have [->|n_neq0] := eqVneq; first by rewrite mul0r mulr0. have [->|d_neq0] := eqVneq; first by rewrite invr0 !mulr0. rewrite !intr_sign invr_sign -signr_addb numq_sign_mul -numq_div_lt0 //. by apply: (canRL (signrMK _)); rewrite mulz_sign_abs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)