proposition: Lemma L_0_2 : rounds standard 0 hinit 2 (hyd1 h3).
proof: Proof. eapply rounds_trans with (h := hyd2 h3 head) (i:=1). - left; trivial. red. cbn. chop_off 1. - left; trivial. red; left; trivial. split; repeat constructor. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)