proposition: Lemma Lab_eq n1 n2 : Lab (nseq n1 a ++ nseq n2 b) -> n1 = n2.
proof: Proof. move => [n H]. by rewrite -[n1](countL _ n2) -{2}[n2](countR n1 n2) H countL countR. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)