proposition: Lemma gnaw_finite : forall n i, gnaw (S n) (iota_from (S i) (S n)) = 0.
proof: Proof. intros; now rewrite iota_from_app, gnaw_app, gnaw_finite_1_iota. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)