proposition: Lemma oppR_lt0 x : 0 < x <-> 0 > - x.
proof: Proof. split; first exact: Ropp_0_lt_gt_contravar. by move/Ropp_gt_lt_contravar; rewrite oppRK oppR0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)