proposition: Lemma largeb_n (n:nat): forall s, ~ In 0 s -> large n s -> (n <= List.length s)%nat.
proof: Proof. induction n. - intros; cbn; auto with arith. - destruct s; cbn. + discriminate. + destruct n0. * destruct 1; now left. * unfold largeb. intro; cbn. destruct n. -- replace (gnaw zero s) with zero. ++ auto with arith. ++ now rewrite gnaw_zero. -- intros; apply le_n_S, IHn. ++ intro;destruct H;auto. ++ auto. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)