proposition: Lemma concP {l1 l2 w} : reflect (exists w1 w2, w = w1 ++ w2 /\ w1 \in l1 /\ w2 \in l2) (w \in conc l1 l2).
proof: Proof. apply: (iffP existsP) => [[n] /andP [H1 H2] | [w1] [w2] [e [H1 H2]]]. - exists (take n w), (drop n w). by rewrite cat_take_drop. - have lt_w1: size w1 < (size w).+1 by rewrite e size_cat ltnS leq_addr. exists (Ordinal lt_w1); subst. rewrite take_size_cat // drop_size_cat //. exact/andP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(misc)