proposition: Lemma Lab_not_regular : ~ inhabited (regular Lab).
proof: Proof. pose f n := nseq n a. apply: (@residualP f) => n1 n2. move/(_ (nseq n2 b)) => H. apply: Lab_eq. apply/H. by exists n2. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)