proposition: Lemma cat_beyond I n (Ns : n.-tuple (seq nat)) X : n <= X -> cat Ns I X = I (X - n).
proof: Proof. move => A. by rewrite /cat size_tuple ltnNge A. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)