proposition: Lemma gnaw_finite_1 : forall n i, gnaw (S n) (interval (S i) (n + i)%nat) = 1.
proof: Proof. intros ; unfold interval. replace (S (n + i) - S i)%nat with n; [| lia]. apply gnaw_finite_1_iota. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)