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