proposition: Lemma i_f_i : forall i:nat, i <= iterate f i 0.
proof: Proof. induction i as [ | n IHn]. - auto with arith. - assert (H0: iterate f n 0 < iterate f (S n) 0). + clear IHn; induction n;simpl;auto. + lia. Qed.
imports: Arith Lia