proposition: Lemma I_of_vev_max k (a:char) w: k \in I_of (vec_of w) (enum_rank a) -> k < size w.
proof: Proof. by rewrite /vec_of /I_of mem_filter mem_iota add0n size_map => /andP[_]. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)