proposition: Lemma step_rounds : forall i a b c a' b' c', one_step i a b c a' b' c' -> rounds standard i (hyd a b c) (S i) (hyd a' b' c').
proof: Proof. destruct 1. - left; trivial; left; split. do 2 apply hcons_mult_S0; now left. - left; trivial; right; left. apply hcons_mult_S1; simpl. rewrite <- hcons_mult_comm. apply hcons_mult_S1. unfold hyd_mult; cbn. left; split; constructor. - left; trivial; right; left. simpl; rewrite <- hcons_mult_comm; apply hcons_mult_S1. left; split; simpl; right; constructor. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)