proposition: Lemma countL n1 n2 : count (pred1 a) (nseq n1 a ++ nseq n2 b) = n1.
proof: Proof. by rewrite count_cat !count_nseq /= eqxx eq_sym (negbTE Hab) mul1n mul0n addn0. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)