proposition: Corollary iterate_gt_diag' : forall i f, dominates_from i f id -> strict_mono f -> forall n, 0 < n -> {j:nat | i<= j /\ dominates_from j (iterate f n) id}.
proof: Proof. destruct n. - intro H1; cut False; [contradiction | lia]. - intros _; apply dominates_iterate; auto. Defined.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)