proposition: Lemma lub_eq_esp_right : forall (f : natO -m> U) (k : U), lub ((UEsp <_> k) @ f) == lub f & k.
proof: Proof. intros; apply Ole_antisym. apply lub_le; auto. apply Uplus_inv_le_esp. rewrite <- lub_eq_plus_cte_right. apply lub_le_compat; simpl; auto. Qed.
imports: ALEA(Utheory)