proposition: Lemma natklub_least : forall (D:cpo) (k:nat) (h:natO-m>natk_ord D k) (p:natk_ord D k), (forall n:nat, h n <= p) -> natklub h <= p.
proof: Proof. simpl; red; unfold natklub; intros. apply lub_le; intros. rewrite natk_mon_shift_simpl. rewrite norm_simpl_lt; auto. apply (H n0 n H0). Qed.