proposition: Lemma phi_less_than_fixpoint : forall phi : A, lub R phi (fun n => iter n bot) -> forall psi : A, psi = f psi -> R phi psi.
proof: Proof. intros phi [Hup Hl] psi Hfxp; apply Hl. intros n; induction n. simpl; auto. simpl; rewrite Hfxp; apply f_monotonic; assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith