proposition: Lemma rex_pumping : forall re s, s \in re -> pumping_constant re <= length s -> RexPump re s.
proof: Proof. intros re s Hmatch. induction Hmatch; simpl; intros Hlen; try lia. - subst. destruct pumping_constant_inv_app_1 with (re1:=re1) (re2:=re2) (s1:=s1) (s2:=s2) as [? | []]; auto using rex_pump_app_l, pump_app_r. - assert (H : pumping_constant re1 <= length s1) by lia. auto using rex_pump_union_l. - assert (H : pumping_constant re2 <= length s2) by lia. auto using rex_pump_union_r. - inversion Hlen as [|?]. apply pumping_constant_neq_0 in H. contradiction. - destruct pumping_constant_inv_app_2 with (s1:=s1) (re:=re) (s2:=s2) as [?|[[]| ?]]; subst; auto using rex_pump_star_1, rex_pump_star_2. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang