proposition: Lemma oppR_eq0 x : (- x == 0) = (x == 0).
proof: Proof. apply/idP/idP => [|/eqP ->]; last by rewrite oppR0. by apply: contraTT; move/eqP/Ropp_neq_0_compat/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)