proposition: Lemma pumping_constant_inv_app_1: forall re1 re2 (s1 s2:word), pumping_constant re1 + pumping_constant re2 <= length (s1 ++ s2) -> pumping_constant re1 <= length s1 \/ (pumping_constant re2 <= length s2 /\ length s1 <= pumping_constant re1).
proof: Proof. intros. rewrite app_length in *. lia. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang