proposition: Lemma lub_le_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 lub_le; intros. apply Ole_trans with (f (n+n0)). apply (fmonotonic f); simpl; auto with arith. apply Ole_trans with (g (n+n0)); auto. apply H; simpl; auto with arith. Qed.