proposition: Lemma step_to_battle : forall p q, step p q -> iota p -+-> iota q.
proof: Proof. destruct 1; [ apply succ_rounds | apply limit_rounds]. Qed.
imports: Coq(Arith Peano_dec Lia Relations Relation_Operators) hydras(Hydra_Lemmas Simple_LexProd ON_Omega2)