proposition: Lemma large_omega_iff : forall s n, ~ In 0 (n::s) -> large T1omega (n::s) <-> (n <= List.length s)%nat.
proof: Proof. intros s n H; split; rewrite large_iff; intro H0. - now apply large_omega_1. - now apply large_omega_2. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)