proposition: Lemma L_cat (X : {set A}) x y z w1 w2 : z \in X -> w1 \in L^X x z -> w2 \in L^X z y -> w1++w2 \in L^X x y.
proof: Proof. move => Hz /LP [H11 H12] /LP [H21 H22]. apply/LP. split; first by rewrite delta_cat H11 H21. move => i i_gt0 H. rewrite take_cat. case: (boolP (i < _)); first exact: H12. rewrite delta_cat H11 -leqNgt => le_w1. case: (posnP (i - size w1)) => [->|Hi]; first by rewrite take0. apply: H22 => //. by rewrite -(ltn_add2l (size w1)) subnKC // -size_cat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)