proposition: Lemma fcont_app_continuous : forall (O:ord) (D1 D2:cpo) (f: O -m> D1-c> D2) (h:natO-m>D1), f <__> (lub h) <= lub (c:=O-M->D2) (fcontit (fmon_fcont_shift f) @ h).
proof: Proof. intros; intro x. rewrite fcont_app_simpl. rewrite (fcontinuous (f x) h); auto. Qed.