proposition: Lemma lub_iterates_fixpoint : forall phi : A, lub R phi (fun n => iter n bot) -> phi = f phi.
proof: Proof. intros phi [Hub Hl]; apply Ha. apply Hl; apply f_phi_upper_bound; assumption. assert (Hfphi : lub R (f phi) (fun n => f (iter n bot))). apply (Hct (fun n => iter n bot) Hchain_iter_f_bot phi);split;assumption. destruct Hfphi as [Hub' Hl']. apply Hl'; apply phi_ub_iter_add_f; assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith