proposition: Lemma drop_accept (w : word char) (i : 'I_(size w)) (q : A) : drop i w \in dfa_accept q = (drop i.+1 w \in dfa_accept (dfa_trans q (tnth (tape w) i))).
proof: Proof. case: w i q => [[//]|a w [m Hm] q]. rewrite [drop]lock (tnth_nth a) /= -lock. elim: {w} (a :: w) m Hm q => [|b w IHw [|m] Hm q]; first by case. by rewrite drop0 drop1. exact: IHw. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)