proposition: Lemma mlarge_omega k : mlarge T1omega (interval (S k) (2 * (S k))%nat).
proof: Proof. specialize (L_lim_ok T1omega nf_omega refl_equal L_fin (fun i => L_fin_ok (S i))). intros. inversion H; auto. unfold L_fin in H1; specialize (H1 k). simpl in H1. now replace ( (2 * S k))%nat with (k + S (S k))%nat by lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)