proposition: Lemma big_plus_size (T char : eqType) (r : seq T) (F : T -> regexp char) m : (forall i, i \in r -> re_size (F i) <= m) -> re_size (\sigma_(i <- r) F i) <= (size r * m.+1).+1.
proof: Proof. elim: r => [|e r IH /forall_cons [A B]]; first by rewrite big_nil. rewrite big_cons /= ltnS mulSn addSn -addnS leq_add //. exact: IH. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)