proposition: Lemma srelL (i j : pos x) p q : srel (size x).+1 x (p,i) (q,j) = srel (size x).+1 (x++z) (p,inord i) (q,inord j).
proof: Proof. case: (boolP (i == (size x).+1 :> nat)) => Hi. - rewrite /srel (eqP Hi) /= inordK ?eqxx //= ?andbF //; ssrlia. - have Hi' : i < (size x).+1. by rewrite ltn_neqAle Hi -ltnS ltn_ord. rewrite /srel /step readL // !inordK //; ssrlia. move: (ltn_ord j) => ?. ssrlia. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)