proposition: Theorem lub_some_witness1 : forall (A:Type) (c:nat -> option A)(v:A), lub (@option_cpo A) (Some v) c -> (exists n:nat, c n = Some v).
proof: Proof. intros A c v [Hup Hl]. elim (classic (forall n, c n = None)). intros Hnone. assert (Hnone_aux : option_cpo (Some v) None). apply Hl. intros n. rewrite Hnone; auto. inversion Hnone_aux. intros Hnot_all. assert (Hex_not : exists n, c n <> None). apply not_all_ex_not with (U:=nat) (P:= fun n => c n = None)(1:= Hnot_all). destruct Hex_not as [n Hneq]. assert (Hopt: option_cpo (c n) (Some v)). apply (Hup n). exists n. inversion Hopt; auto. elim Hneq; auto. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith