proposition: Lemma iterate2_mono2 (phi psi : (nat->nat)->(nat->nat)): (forall g, strict_mono g -> S <<= g -> strict_mono (phi g))-> (forall g, strict_mono g -> S <<= g -> S <<= (phi g))-> (forall g, strict_mono g -> S <<= g -> strict_mono (psi g))-> (forall g, strict_mono g -> S <<= g -> S <<= (psi g))-> (forall g x, strict_mono g -> fun_le S g -> phi g x <= psi g x) -> (forall f g, strict_mono f -> strict_mono g -> S <<= f -> S <<= g -> (forall x, f x <= g x) -> (forall x, psi f x <= psi g x)) -> forall k g x y, strict_mono g -> S <<= g -> (x <= y)%nat -> (iterate phi k g x <= iterate psi k g y)%nat.
proof: Proof. induction k. - simpl; intros g x y H5 H6 H7; destruct (Nat.lt_eq_cases x y) as [H8 H9]. destruct (H8 H7). + apply Nat.lt_le_incl. apply H5; auto. + subst; auto. - intros; repeat rewrite iterate_S_eqn2. transitivity (iterate psi k (psi g) x). + specialize (IHk (phi g) x x (H g H5 H6) (H0 g H5 H6)). transitivity (iterate psi k (phi g) x). * apply IHk; auto. * apply iterate2_mono3; auto. + apply iterate2_mono3; auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)