proposition: Lemma iterate2_mono_weak (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. intros g Hg k g0 x y Hmono ? Hxy. destruct (Nat.lt_eq_cases x y) as [H4 H5]; apply H4 in Hxy. destruct Hxy. - apply Nat.lt_le_incl, iterate2_mono; auto. - now subst. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)