proposition: Theorem Rle_bool_false : forall x y, (y < x)%R -> Rle_bool x y = false.
proof: Proof. intros x y Hxy. case Rle_bool_spec ; intros H. elim (Rlt_irrefl x). now apply Rle_lt_trans with y. apply refl_equal. Qed.
imports: Coq(Psatz Reals ZArith) Zaux