proposition: Lemma L_split X p q z w : w \in L (z |: X) p q -> w \in L^X p q \/ exists w1 w2, [/\ w = w1 ++ w2, size w2 < size w, w1 \in L^X p z & w2 \in L^(z |: X) z q].
proof: Proof. case/LP => H1 H2. case: (find_minn_bound (fun i => (0 < i) && (delta p (take i w) == z)) (size w)). - case => i [lt_w /andP [i_gt0 /eqP delta_z] min_i]; right. exists (take i w); exists (drop i w). have ? : 0 < size w by exact: ltn_trans lt_w. rewrite cat_take_drop size_drop -{2}[size w]subn0 ltn_sub2l //; split => //. + apply/LP. split => // j J1 J2. have lt_i_j : j < i. apply: leq_trans J2 _. by rewrite size_take lt_w. have/(H2 _ J1) : j < size w. exact: ltn_trans lt_w. case/setU1P => [H|]; last by rewrite take_takel 1?ltnW. move: (min_i _ lt_i_j). by rewrite negb_and J1 H eqxx. + apply/LP. rewrite -H1 -{2}[w](cat_take_drop i) delta_cat delta_z. split => // j J1 J2. rewrite -{1}delta_z -delta_cat -takeD. apply: H2; first by rewrite addn_gt0 J1 orbT. by rewrite -[w](cat_take_drop i) size_cat size_take lt_w ltn_add2l. - move => H; left. apply/LP. split => // i I1 I2. apply: contraTT (H2 _ I1 I2) => C. rewrite inE negb_or C inE andbT. apply: contraNN (H _ I2) => ->. by rewrite I1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)