proposition: Lemma mg_right_congruent L (N : mgClassifier L) : right_congruent N.
proof: Proof. move => u v a /nerodeP H. apply/nerodeP => w. by rewrite -!catA. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)