proposition: Lemma lub_lift_left : forall (D:cpo) (f:natO -m> D) n, lub f == lub (mseq_lift_left f n).
proof: Proof. intros; apply Ole_antisym; auto. apply lub_le_compat; intro. unfold mseq_lift_left; simpl. apply (fmonotonic f); auto with arith. Qed.