proposition: Lemma nfa2_of_aux2 (q f:A) (i : pos w) : i != ord0 -> f \in nfa2_f nfa2_of_dfa -> connect (step nfa2_of_dfa w) (q,i) (f,ord_max) -> ((drop i.-1 w) \in dfa_accept q).
proof: Proof. move => H fin_f. case/connectP => p. elim: p i H q => //= [|[q' j] p IHp i Hi q]. - move => i Hi q _ [<- <-]. rewrite drop_size -topredE /= accept_nil. by rewrite inE in fin_f. - rewrite {1}/step /read. case: (ord2P i) => /= [|/eqP->|i' Hi']; try by rewrite ?inE ?(negbTE Hi). rewrite !inE !xpair_eqE (_ : L == R = false) ?eqxx ?andbT ?andbF ?orbF -?andbA //=. case/and3P => /eqP -> /eqP E. rewrite -Hi' drop_accept. have -> : i'.+1 = j.-1 by rewrite E. apply IHp. by apply: contra_eq_neq E =>->. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)