proposition: Lemma cards_lt1 (T : finType) (A : {set T}) : #|A| <= 1 -> A = set0 \/ exists x, A = [set x].
proof: Proof. move => H. case (posnP #|A|) => H'. - left. exact:cards0_eq. - right. apply/cards1P. by rewrite eqn_leq H H'. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)