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