proposition: Theorem Rcompare_Gt : forall x y, (y < x)%R -> Rcompare x y = Gt.
proof: Proof. intros x y H. case Rcompare_spec ; intro H'. elim (Rlt_irrefl x). now apply Rlt_trans with y. rewrite H' in H. elim (Rlt_irrefl _ H). easy. Qed.
imports: Coq(Psatz Reals ZArith) Zaux