proposition: Lemma realEsg x : x \is real -> x = sgr x * `|x|.
proof: Proof. move=> xR; have [-> | ] := eqVneq x 0; first by rewrite normr0 mulr0. by move=> /neqr0_sign <-; rewrite -realEsign. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)