proposition: Lemma limit_rounds_0 : forall i j, round_n j (iota (S i, 0)) (iota (i, S j)).
proof: Proof. intros i j; destruct i. - unfold iota; right; left; change (hcons head (hcons_mult head j hnil)) with (hcons_mult head (S j) hnil). left; split; left. - right; left; cbn; rewrite <- hcons_mult_comm; right. apply hcons_mult_S1; left; split; constructor. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)