proposition: Lemma natklub_less : forall (D:cpo) (k:nat) (h:natO-m>natk_ord D k) (n:nat), h n <= natklub h.
proof: Proof. simpl; red; unfold natklub; intros. apply Ole_trans with (natk_mon_shift (O1:=natO) (O2:=D) 0 (k:=k) h n0 n); auto. rewrite natk_mon_shift_simpl. rewrite norm_simpl_lt; auto. Qed.