proposition: Theorem least_fixpoint_lub_iterates : forall phi, least_fixpoint f phi -> lub R phi (fun n => iter n bot).
proof: Proof. intros phi Hlfp. destruct (Hc (fun n => iter n bot) Hchain_iter_f_bot) as [psi Hlub']. replace phi with psi. trivial. symmetry. apply least_unique with (1:= Ha) (P:= fun x => x = f x) (2:= Hlfp). split. apply lub_iterates_fixpoint; auto. apply phi_less_than_fixpoint; auto. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith