proposition: Lemma readL x z (p:M) (k : pos x) : k != (size x).+1 :> nat -> read p (inord k : pos (x++z)) = read p k.
proof: Proof. move => Hk. rewrite /read. case: (ord2P k) => [/eqP->|E|i Hi]. - by rewrite /= -inord0 ord2P0. - apply: contraN Hk. by rewrite (eqP E). - have oi : i < size (x++z) by rewrite size_cat ltn_addr. have H_eq: (Ordinal oi).+1 = (inord k : pos (x++z)). by rewrite -Hi inordK // ; ssrlia. by rewrite (ord2PC H_eq) -(tnthL (i := i)). Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)