proposition: Lemma glb_half_exp : glb (UExp [1/2]) == 0.
proof: Proof. unfold glb; apply Uinv_eq_perm_left. apply Oeq_trans with (lub U1min). apply lub_eq_compat; apply fmon_eq_intro; simpl; unfold U1min,pmin; simpl; auto. rewrite eq_lim_U1min; auto. Qed.
imports: ALEA(Utheory)