proposition: Lemma iterate_mono_1 (f g: nat -> nat) (k:nat) (Hf: strict_mono f) (Hf' : S <<= f) (H : forall n, k <= n -> f n <= g n) : forall i n, k <= n -> iterate f i n <= iterate g i n.
proof: Proof. induction i. - simpl; auto with arith. - intros; repeat rewrite iterate_S_eqn. transitivity (f (iterate g i n)); auto. + apply mono_weak; auto. + apply H; transitivity (iterate f i n); [ | auto]. * induction H0. -- clear IHi; induction i. ++ simpl; auto with arith. ++ rewrite iterate_S_eqn. transitivity (iterate f i k). ** auto. ** apply Nat.lt_le_incl; auto. -- transitivity (S m). ++ auto with arith. ++ apply iterate_ge; auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)