proposition: Lemma reachable_S : forall i a b, reachable i a (S b) 0 -> reachable (doubleS i) a b 0.
proof: Proof. intros; right with (1 := H); apply doubleS_law. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)