proposition: Lemma real_ler_norml x y : x \is real -> (`|x| <= y) = (- y <= x <= y).
proof: Proof. move=> xR; wlog x_ge0 : x xR / 0 <= x => [hwlog|]. move: (xR) => /(@real_leVge 0) /orP [|/hwlog->|hx] //. by rewrite -[x]opprK normrN lerN2 andbC lerNl hwlog ?realN ?oppr_ge0. rewrite ger0_norm //; have [le_xy|] := boolP (x <= y); last by rewrite andbF. by rewrite (le_trans _ x_ge0) // oppr_le0 (le_trans x_ge0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)