proposition: Lemma Rle_plus_epsilon : forall r1 r2, (forall eps:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.
proof: Proof. intros r1 r2 H. destruct (Rle_or_lt r1 r2) as [r1_le_r2 | r1_gt_r2]; [assumption |]. exfalso. destruct (Rexists_between r2 r1) as [r [r2_lt_r r_lt_r1]]; [assumption |]. apply (Rlt_irrefl r1), (Rle_lt_trans _ r); [| assumption]. rewrite <-(Rplus_minus r2 r). now apply H, Rgt_minus. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField