proposition: Lemma large_omega_1 : forall s n, ~ In 0 (n::s) -> gnaw T1omega (n::s) = 0 -> (n <= List.length s)%nat.
proof: Proof. intros s n; destruct n. - auto with arith. - intros H H0; cbn in H0. generalize (largeb_n (S n) s). intros. apply H1;auto. intro; destruct H; now right. unfold largeb. rewrite FS_rw in H0. red. red. unfold largeb. rewrite H0. auto. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)