proposition: Lemma Rcompare_opp : forall x y, Rcompare (- x) (- y) = Rcompare y x.
proof: Proof. intros x y. destruct (Rcompare_spec y x); destruct (Rcompare_spec (- x) (- y)); try reflexivity; exfalso; lra. Qed.
imports: Coq(Psatz Reals ZArith) Zaux