proposition: Lemma lub_eq_plus_cte_left : forall (f:natO -m> U) (k:U), lub ((UPlus k) @ f) == k + lub f.
proof: Proof. intros; apply Oeq_sym; apply lub_comp_eq with (f:=UPlus k) (h:=f); red; intros; auto. Qed.
imports: ALEA(Utheory)