proposition: Lemma read1 x (p:M) (j:pos x) : read p j = set0 \/ exists s : M * dir, read p j = [set s].
proof: Proof. rewrite /read. case: (ord2P _) => [||i] _;apply cards_lt1; rewrite ?cardsX ?cards1 ?muln1; [auto using detL, detC, detR, dfa2_det..|]. exact/detC/dfa2_det. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)