proposition: Theorem comp_right_continuous : forall (A:Type)(f:A->option A), continuous (f_order' A)(f_order' A)(comp_right f).
proof: Proof. intros A f c Hc l [Hu Hl]. split. intros n x; unfold comp_right; case (f x); [exact (Hu n) | apply option_cpo_none_bot]. intros g' Hu' x. assert (Hc' : forall n, option_cpo (comp_right f (c n) x) (comp_right f (c (S n)) x)). intros n; unfold comp_right; case (f x); [intros a; exact (Hc n a) | apply option_cpo_none_bot]. case_eq (f x). intros a Hfxeqa. unfold comp_right; rewrite Hfxeqa. generalize (lub_lift_reverse A (option A) (option_cpo (A:=A)) c l (conj Hu Hl) a). intros [_ Hlla]. apply Hlla. intros n; generalize (Hu' n x); unfold comp_right; rewrite Hfxeqa; trivial. intros Hfxeqnone; unfold comp_right; rewrite Hfxeqnone. apply option_cpo_none_bot. Qed.
imports: Relations Classical ClassicalEpsilon Zwf function_cpo