proposition: Theorem Tarski_fix_prop : forall (A B:Type) (f : (A -> option B)->A -> option B), continuous (f_order A B)(f_order A B) f -> least_fixpoint (f_order A B) f (Tarski_fix f).
proof: Proof. intros A B f Hct; unfold Tarski_fix. apply epsilon_spec. assert (Ht := Tarski_least_fixpoint). apply Tarski_least_fixpoint with (R:=f_order A B) (bot:=fun x:A=>@None B) (4:= (fun (g:A->option B) x => @option_cpo_none_bot B (g x))). apply reflexive_f_order. apply antisymmetric_f_order. apply complete_f_order. exact Hct. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith