proposition: Lemma f_phi_upper_bound : forall phi : A, upper_bound R phi (fun n => iter n bot) -> upper_bound R (f phi) (fun n => iter n bot).
proof: Proof. intros phi Hup [ | p]. apply Hb. apply (f_monotonic (iter p bot)); apply (Hup p). Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith