proposition: Lemma real_ltr_norml x y : x \is real -> (`|x| < y) = (- y < x < y).
proof: Proof. move=> Rx; wlog x_ge0 : x Rx / 0 <= x => [hwlog|]. move: (Rx) => /(@real_leVge 0) /orP [|/hwlog->|hx] //. by rewrite -[x]opprK normrN ltrN2 andbC ltrNl hwlog ?realN ?oppr_ge0. rewrite ger0_norm //; have [le_xy|] := boolP (x < y); last by rewrite andbF. by rewrite (lt_le_trans _ x_ge0) // oppr_lt0 (le_lt_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)