proposition: Lemma doubleS_law : forall a b i, steps i a (S b) 0 (doubleS i) a b 0.
proof: Proof. intros; eapply steps_S. + eleft; apply step2. + unfold doubleS; replace (2 * S i) with (S i + S i) by ring; apply LS. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)