proposition: Theorem Rcompare_sym : forall x y, Rcompare x y = CompOpp (Rcompare y x).
proof: Proof. intros x y. destruct (Rcompare_spec y x) as [H|H|H]. now apply Rcompare_Gt. now apply Rcompare_Eq. now apply Rcompare_Lt. Qed.
imports: Coq(Psatz Reals ZArith) Zaux