proposition: Theorem lub_some_witness : forall (A B:Type) c (a:A)(b:B)(f:A->option B), f a = Some b -> lub (lift_order A (option B) (option_cpo (A:=B))) f c -> (exists n:nat, c n a = Some b).
proof: Proof. intros A B c a b f Heq Hlub. apply (lub_some_witness1 B (fun n => c n a) b). assert (Hlub':= lub_lift_reverse A _ (@option_cpo B) c f Hlub a). rewrite <- Heq; assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith