proposition: Lemma real_eqr_norml x y : x \is real -> (`|x| == y) = ((x == y) || (x == -y)) && (0 <= y).
proof: Proof. move=> Rx. apply/idP/idP=> [|/andP[/pred2P[]-> /ger0_norm/eqP]]; rewrite ?normrE //. case: real_le0P => // hx; rewrite 1?eqr_oppLR => /eqP exy. by move: hx; rewrite exy ?oppr_le0 eqxx orbT //. by move: hx=> /ltW; rewrite exy eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)