proposition: Lemma steps_rounds : forall i a b c j a' b' c', steps i a b c j a' b' c' -> rounds standard i (hyd a b c) j (hyd a' b' c').
proof: Proof. induction 1. - now apply step_rounds. - eapply rounds_trans. + apply IHsteps2. + assumption. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)