proposition: Lemma dlub_lift_right : forall (D:dcpo) (f:natO-m>D) n, dlub f == dlub (mseq_lift_right f n).
proof: Proof. intros; apply Ole_antisym; auto. apply dlub_le_compat; intro. unfold mseq_lift_right; simpl. apply (fmonotonic f); auto with arith. Qed.