proposition: Lemma srelS k x p q (i j : pos x) m : i <= k -> connect (srel k x) (p,i) (q,j) -> connect (srel (k+m) x) (p,i) (q,j).
proof: Proof. move => H /connectP [cs]. elim: cs p i H => [/= p i H _ [-> ->] //|[p' i'] cs IH p i H /= /andP [s pth] l]. have Hk: i < k. case/andP : s => _ /= s. by rewrite ltn_neqAle H eq_sym s. apply: (connect_trans (y := (p',i'))) (connect1 _) _; first by rewrite -srelSr. apply: IH => //. move/srel1 : s Hk => /= s. exact: leq_trans. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)