proposition: Lemma ltrgt0P x : comparer0 x (min 0 x) (min x 0) (max 0 x) (max x 0) `|x| (0 == x) (x == 0) (x <= 0) (0 <= x) (x < 0) (x > 0).
proof: Proof. exact: real_ltgt0P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)