proposition: Lemma iterate_ge' : forall f, id <<= f -> forall n j, 0 < n -> j <= iterate f n j.
proof: Proof. induction n /r. - inversion 2. - intros * H0; destruct n /r. + simpl; intros /n. apply h_fun_le_id_. + intros /n; transitivity (iterate f (S n) j). * auto with arith. * simpl; apply h_fun_le_id_. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)