proposition: Lemma Hchain_iter_f_bot : chain R (fun n => iter n bot).
proof: Proof. unfold chain. induction n. simpl. apply Hb. apply (f_monotonic (iter n bot) (iter (S n) bot)). assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith