fact: Fixpoint re_size (char: eqType) (e : regexp char) := match e with | Star s => (re_size s).+1 | Plus s t => ((re_size s)+(re_size t)).+1 | Conc s t => ((re_size s)+(re_size t)).+1 | _ => 1 end.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)