proposition: Lemma iterate_ge_from : forall f i, dominates_from i f id -> forall j, i <= j -> forall n, j <= iterate f n j.
proof: Proof. induction n. cbn. auto with arith. apply PeanoNat.Nat.lt_le_incl. rewrite iterate_S_eqn. apply Nat.le_lt_trans with (iterate f n j). auto. apply H. apply Nat.le_trans with j. auto. auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)