proposition: Lemma readR (q:M) k : k != 0 -> k < (size z).+2 -> read q (inord k : pos z) = read q (inord (size x + k) : pos (x++z)).
proof: Proof. move => Hk0 Hk. rewrite /read. case: (ord2P _) => [H|H|i Hi]. - apply: contraN Hk0. move/eqP/(f_equal (@nat_of_ord _)) : H => /=. by rewrite inordK // => ->. - by rewrite -[k](@inordK (size z).+1) ?(eqP H) //= addnS -size_cat -inord_max ord2PM. - have Hi' : size x + i < size (x ++ z) by rewrite size_cat ltn_add2l. have X: (Ordinal Hi').+1 = (inord (size x + k) : pos (x ++ z)). by rewrite /= -addnS Hi !inordK //; ssrlia. by rewrite (ord2PC X) -(tnthR (i := i)). Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)