proposition: Lemma gnaw_last_step alpha s i : gnaw alpha s = 1 -> gnaw alpha (s ++ S i :: nil) = 0.
proof: Proof. intro H; now rewrite gnaw_app, H. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)