proposition: Lemma lub_eq_lift : forall (D:cpo) (f g:natO -m> D) (n:natO), (forall k, n <= k -> f k == g k) -> lub f == lub g.
proof: Proof. intros; apply Ole_antisym; apply lub_le_lift with n; intros; auto. apply Oeq_le_sym; auto. Qed.