proposition: Lemma iterate_ge'' f : id <<= f -> strict_mono f -> forall i k, k <= Nat.pred (iterate (fun z => S (f z)) (S i) k).
proof: Proof. induction i /n. - intros; cbn; apply h_fun_le_id_. - intros *; rewrite iterate_rw; apply Nat.le_trans with (Nat.pred (iterate (fun z : nat => S (f z)) (S i) k)). + auto. + cbn; assert (H1: strict_mono (fun z => S (f z))). { intros x y Hlt. apply h_strict_mono_ in Hlt; auto with arith. } generalize (iterate_mono _ H1). assert (H2: S <<= (fun z : nat => S (f z))). { intro x; auto with arith. specialize (h_fun_le_id_ x); auto with arith. } intros H3; specialize (H3 H2 i). apply Nat.lt_le_incl. assert (H4: k < S (f k)). { apply Nat.le_lt_trans with (f k). - apply h_fun_le_id_. - auto with arith. } specialize (H3 _ _ H4); auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)