proposition: Lemma delta_s_right_congruent : right_congruent (delta_s A).
proof: Proof. move => u v a H. rewrite /= /delta_s !delta_cat. by f_equal. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)