proposition: Lemma nfa2_of_aux (q:A) i : i < (size w).+1 -> ((drop i w) \in dfa_accept q) -> [exists f in nfa2_f nfa2_of_dfa, connect (step nfa2_of_dfa w) (q,inord i.+1) (f,ord_max)].
proof: Proof. move eq_m : (n - i) => m. elim: m q i eq_m => [|m IHm] q i /eqP H1 H2. - have/eqP -> : i == (size w). by rewrite eqn_leq -ltnS H2 -subn_eq0 H1. rewrite drop_size unfold_in -inord_max /= => F. apply/existsP;exists q. rewrite inE F. exact: connect0. - move => H. have Hi : i < size w. { rewrite ltn_neqAle -ltnS H2 andbT. apply: contraTN H1 => /eqP->. by rewrite subnn. } have Hm : n - i.+1 = m by apply/eqP;rewrite subnS (eqP H1). move/(_ (dfa_trans q (tnth (tape w) (Ordinal Hi))) _ Hm Hi) : IHm. rewrite -[i.+1]/(Ordinal Hi).+1 -drop_accept. move => /(_ H). case/exists_inP => f f1 f2. apply/exists_inP;exists f => //. apply: connect_trans (connect1 _) f2. rewrite /step /read (ord2PC (i' := (Ordinal Hi))) ?inordK //= => _. by rewrite inE ?eqxx. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)