proposition: Lemma double_lub_diag : forall (D:cpo) (h:natO-m>natO-M->D), lub (lub h) == lub (fmon_diag h).
proof: Proof. intros. intros; apply Ole_antisym. apply lub_le; intros; simpl; apply lub_le; intros; simpl. apply Ole_trans with (h (n+n0) (n+n0)); auto with arith. apply le_lub with (f:=fmon_diag h) (n:=(n + n0)%nat). apply lub_le_compat. unfold fmon_diag; simpl; intros. apply le_lub with (f:=h <_> x) (n:=x). Qed.