proposition: Lemma LS : forall c a b i, steps i a b (S c) (i + S c) a b 0.
proof: Proof. induction c. - intros; replace (i + 1) with (S i) by ring. repeat constructor. - intros; eapply steps_S. + eleft; apply step1. + replace (i + S (S c)) with (S i + S c) by ring; apply IHc. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)