proposition: Lemma srelRE m k p c : k < (size z).+2 -> k != 0 -> srel m (x++z) (p,inord (size x + k)) c -> exists q k', k' < (size z).+2 /\ c = (q,inord (size x + k')).
proof: Proof. move: k c => [//|k] [q j] Hk _ /srelLR [/eqP C|/eqP C]; exists q; rewrite inordK addnS ?eqSS in C; ssrlia. - exists k. by rewrite ltnW // -[j]inord_val (eqP C). - exists k.+2. rewrite !addnS -[j]inord_val (eqP C). split => //. rewrite eqn_leq in C. case/andP : C => _ C. move: (leq_ltn_trans C (ltn_ord j)). by rewrite size_cat -!addnS leq_add2l. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)