proposition: Lemma iterate2_mono3 (phi : (nat->nat)->(nat->nat)) : (forall g, strict_mono g -> S <<= g -> strict_mono (phi g) /\ S <<= phi g)-> (forall (f g : nat -> nat), strict_mono f -> S <<= f -> strict_mono g -> S <<= g -> ((forall x, f x <= g x) -> forall x, phi f x <= phi g x)) -> forall g h, strict_mono g -> S <<= g -> strict_mono h -> S <<= h -> (forall x, g x <= h x) -> forall k x y, x <= y -> iterate phi k g x <= iterate phi k h y.
proof: Proof. intros; revert k x y H6. assert (H6: forall k, strict_mono (iterate phi k h) /\ S <<= iterate phi k h). { intro k; induction k. - simpl; split; auto. - destruct IHk; split. + simpl; destruct (H (iterate phi k h)); auto. + simpl; destruct (H (iterate phi k h)); auto. } assert (H7: forall k, strict_mono (iterate phi k g) /\ S <<= iterate phi k g). { { intro k; induction k. - simpl; split; auto. - destruct IHk; split. + simpl; destruct (H (iterate phi k g)); auto. + simpl; destruct (H (iterate phi k g)); auto. } } induction k. - simpl; intros; transitivity (g y). + apply mono_weak; auto. + auto. - intros; repeat rewrite iterate_S_eqn; transitivity (phi (iterate phi k h) x). + apply H0. * destruct (H7 k); auto. * destruct (H7 k); auto. * destruct (H6 k); auto. * destruct (H6 k); auto. * intro; apply IHk; auto with arith. + clear IHk; destruct (H6 k). destruct (H (iterate phi k h) H9 H10); apply mono_weak; auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)