proposition: Lemma succ_rounds : forall i j, iota (i,S j) -+-> iota (i, j).
proof: Proof. unfold iota; left; exists 0; left; split; apply hcons_mult_S0; constructor. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)