proposition: Lemma L_omega : forall k, L_ E0_omega k = S (2 * k)%nat.
proof: Proof. intro k; rewrite L_lim_eqn. - replace (Canon E0_omega k) with (E0fin k). + rewrite L_finite; abstract lia. + cbn; unfold Canon; cbn. apply E0_eq_intro. destruct k; reflexivity. - now cbn. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)