proposition: Lemma pumping_constant_inv_app_2: forall s1 re (s2:list ascii), pumping_constant re <= length (s1 ++ s2) -> s1 = [] \/ (s1 <> [] /\ length s1 <= pumping_constant re) \/ pumping_constant re <= length s1.
proof: Proof. intros. rewrite app_length in *. destruct s1. { intuition. } right. destruct (PeanoNat.Nat.lt_ge_cases (length (a :: s1)) (pumping_constant re)). { simpl in *. left. split. { intros N; inversion N. } auto using PeanoNat.Nat.lt_le_incl. } right. assumption. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang