proposition: Lemma Tab_rc : right_congruent Tab.
proof: Proof. move => x y a E. have Tab2 : (Tab (x ++ [:: a])).2 = (Tab (y ++ [:: a])).2. { apply/setP => [[p q]]. rewrite /Tab !inE /= !inord_max. apply/idP/idP; apply: (runR_eq (i := 1) (j := 2) (k := 1)); by rewrite ?size_cat ?addn1 ?addn2. } suff ?: (Tab (x ++ [:: a])).1 = (Tab (y ++ [:: a])).1 by congr pair. apply/setP => q /=. rewrite !inE. pose C x := connect (srel (size (x ++ [:: a])).+1 (x ++ [:: a])) (nfa2_s M, ord1) (q, ord_max). wlog suff W: x y E Tab2 / C x -> C y; [by apply/idP/idP; exact: W|]. case/(@srel_mid (size x).+1); ssrlia => p /Tab1P p1 p2. apply/(@srel_mid (size y).+1); ssrlia. exists p; first by apply/Tab1P; rewrite -E. move: p2. rewrite -![_.+1 as X in inord X]addn1 -[1]/(size [:: a]) -!size_cat. rewrite !(@runL _ [::]) !inordK; ssrlia. move/Tab2P => p2. by apply/Tab2P; rewrite -Tab2. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)