proposition: Lemma limit_rounds : forall i j, iota (S i, 0) -+-> iota (i, j).
proof: Proof. intros i j; apply round_plus_trans with (iota (i, S j)). - left; exists j; apply limit_rounds_0. - apply succ_rounds. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)