proposition: Theorem Tarski_fix_iterates_witness : forall (A B:Type) (f : (A -> option B)->A -> option B), continuous (f_order A B)(f_order A B) f-> forall (x:A)(v:B), Tarski_fix f x = Some v -> exists n, iter (A->option B) f n (fun a => None) x = Some v.
proof: Proof. intros A B f Hct x. assert (H:lub (f_order A B) (Tarski_fix f) (fun n => iter _ f n (fun a=>None))). apply least_fixpoint_lub_iterates. apply reflexive_f_order. apply antisymmetric_f_order. apply complete_f_order. intros g y; apply option_cpo_none_bot. assumption. apply Tarski_fix_prop. assumption. intros v Heq. apply lub_some_witness with (A:=A)(B:=B)(1:= Heq)(2:=H). Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith