proposition: Lemma Ule_lt_half_exp : forall x y, (forall p, x <= y + [1/2]^p) -> x <= y.
proof: Proof. intros; apply Ole_trans with (glb (UExp [1/2]) + y). apply Ole_trans with (glb (Imon (UPlus <_> y) @ (UExp [1/2]))). apply le_glb; intro p; apply Ole_trans with (y + [1/2] ^ p); auto. rewrite glb_eq_plus_cte_right; auto. rewrite glb_half_exp; auto. Qed.
imports: ALEA(Utheory)