proposition: Lemma real_ler_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_leF ?realN. rewrite real_leNgt ?real_ltr_norml // negb_and -?real_leNgt ?realN //. by rewrite orbC lerNr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)