proposition: Lemma image_rc : right_congruent Tab'.
proof: Proof. move => x y a /(congr1 val) /= E. apply: val_inj. exact: Tab_rc. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)