proposition: Lemma strict_mono_iterate_S f : strict_mono f -> id <<= f -> forall i, strict_mono (fun k => Nat.pred (iterate (fun z => S (f z)) (S i) k)).
proof: Proof. intros Hmono Hle; induction i. - cbn; apply Hmono. - intros k l Hlt. assert (H: k <= Nat.pred (iterate (fun z : nat => S (f z)) (S (S i)) k)) by (apply iterate_ge''; auto). assert (H0: k < iterate (fun z : nat => S (f z)) (S (S i)) k). { replace k with (iterate (fun z => S (f z)) 0 k) at 1. - apply iterate_lt. + intros x y Hxy; specialize (Hmono _ _ Hxy); auto with arith. + intros x; auto with arith; specialize (Hle x); auto with arith. + auto with arith. - reflexivity. } rewrite <- Nat.pred_lt_mono. + apply iterate_mono. * intros x y Hxy; specialize (Hmono _ _ Hxy); auto with arith. * intros x; specialize (Hle x); auto with arith. * auto. + intro H1; rewrite H1 in H0; inversion H0. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)