proposition: Theorem Rlt_bool_spec : forall x y, Rlt_bool_prop x y (Rlt_bool x y).
proof: Proof. intros x y. unfold Rlt_bool. case Rcompare_spec ; constructor. exact H. rewrite H. apply Rle_refl. now apply Rlt_le. Qed.
imports: Coq(Psatz Reals ZArith) Zaux