proposition: Lemma round_S: forall i n, battle_rel free n (iota (S i)) (iota i).
proof: Proof. intros i n; exists 0; constructor 1; constructor; induction i. - right;left. - cbn; constructor 2; trivial. Qed.
imports: Coq(Arith Lia) hydras(Hydra_Lemmas ON_Generic ON_Omega)