proposition: Lemma real_le0P x : x \is real -> ler0_xor_gt0 x (min 0 x) (min x 0) (max 0 x) (max x 0) `|x| (0 < x) (x <= 0).
proof: Proof. move=> hx; rewrite -[X in `|X|]subr0; case: real_ltP; by rewrite ?subr0 ?sub0r //; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)