proposition: Lemma gnaw_n_R : forall s n, ~ In 0 s -> (n < List.length s)%nat -> gnaw (S n) s = zero.
proof: Proof. induction s. - cbn; intros; destruct n; inversion H0. - cbn; destruct n. + cbn; auto. destruct a. * destruct 1; auto. * now rewrite gnaw_zero. + intros H; destruct a. * destruct H; auto. * intro; apply IHs; [tauto | auto with arith]. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)