proposition: Lemma prop_eps : forall r:R, (forall eps:R, eps > 0 -> r < eps) -> r <= 0.
proof: Proof. intros; elim (Rtotal_order r 0); intro. - apply Rlt_le; assumption. - elim H0; intro. + apply Req_le; assumption. + clear H0; generalize (H r H1); intro; generalize (Rlt_irrefl r); intro; exfalso; auto. Qed.
imports: Rbase Rfunctions Lra