proposition: Theorem Tarski_least_fixpoint : exists phi: A, least_fixpoint f phi.
proof: Proof. destruct (Hc (fun n => iter n bot) Hchain_iter_f_bot) as [phi Hlub]. exists phi. split. apply lub_iterates_fixpoint; auto. apply phi_less_than_fixpoint; auto. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith