proposition: Lemma real_ltr_normr x y : y \is real -> (x < `|y|) = (x < y) || (x < - y).
proof: Proof. move=> Ry. have [xR|xNR] := boolP (x \is real); last by rewrite ?Nreal_ltF ?realN. rewrite real_ltNge ?real_ler_norml // negb_and -?real_ltNge ?realN //. by rewrite orbC ltrNr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)