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