proposition: Lemma srelSr k' k x (c d : nfa2_config M x) : c.2 < k -> srel k x c d = srel (k+k') x c d.
proof: Proof. move => lt_k. by rewrite /srel !neq_ltn ltn_addr lt_k ?orbT. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)