proposition: Lemma large_n_iff : forall s (n:nat) , ~ In 0 s -> large n s <-> (n <= List.length s)%nat.
proof: Proof. split. - now apply largeb_n. - destruct n. + unfold large, largeb; cbn; now rewrite gnaw_zero. + unfold large; now apply largeb_n_R. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)