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