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