proposition: Lemma srelR (m k k' : nat) p p' : k != 0 -> k < (size z).+2 -> k' < (size z).+2 -> srel ((size x).+1 + m) (x++z) (p,inord (size x + k)) (p',inord (size x + k')) = srel m.+1 z (p,inord k) (p',inord k').
proof: Proof. move => Hk0 Hk Hk'. rewrite /srel /= !inordK ?addSnnS ?eqn_add2l //; ssrlia. case: (_ != _); rewrite ?andbT ?andbF // /step -?readR //. rewrite !inordK //; ssrlia. by rewrite -!addnS !eqn_add2l. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)