proposition: Lemma iterate2_mono (f : (nat->nat)->(nat->nat)): (forall g, strict_mono g -> S <<= g -> strict_mono (f g))-> (forall g, strict_mono g -> S <<= g -> S <<= (f g))-> forall k g x y, strict_mono g -> S <<= g -> (x < y)%nat -> (iterate f k g x < iterate f k g y)%nat.
proof: Proof. induction k. - cbn; intros; apply (H1 _ _ H3); auto. - intros; rewrite iterate_S_eqn2. apply (IHk (f g) x y ); auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)