proposition: Lemma eqR_opp x y : (- x == - y) = (x == y).
proof: Proof. by apply/eqP/eqP => [Hopp|->//]; rewrite -[LHS]oppRK -[RHS]oppRK Hopp. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)