proposition: Lemma L_2_3 : rounds standard 2 (hyd1 h3) 3 (hyd 3 0 0).
proof: Proof. left; trivial; right ; simpl; left; left. split; right; right; left. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)