proposition: Theorem pumping: forall L, Regular L -> exists p, p >= 1 /\ forall w, In w L -> length w >= p -> In w (Pump L p).
proof: Proof. intros. inversion H; subst; clear H. exists (pumping_constant r). split. { apply pumping_constant_ge_1. } intros. assert (RexPump r w). { apply rex_pumping. + apply H0. assumption. + lia. } apply rex_pump_to_pump; auto. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util