proposition: Lemma size_glue b n (v : seq (vec n)) : size (glue b v) = maxn (size b) (size v).
proof: Proof. elim: b v => [|b bs IH] v /=; first by rewrite max0n size_map. case: v => [|v vs]; by rewrite /= ?maxnSS IH ?maxn0. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)