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