proposition: Theorem complete_option_cpo : complete option_cpo.
proof: Proof. intros f Hchain. elim (classic (forall n, f n = None)). intros Hn; exists (None (A:=A)). split; intros p; try rewrite Hn; auto. intros Hnotforall. elim not_all_ex_not with (P:= fun x => f x = None) (1:= Hnotforall). intros n Hneq; exists (f n); split; [auto | intros y; auto]. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith