proposition: Lemma ord2P0 n : ord2P (@ord0 n.+1) = Ord20 (eqxx _).
proof: Proof. case: (ord2P (@ord0 n.+1)) => //= H. congr Ord20. exact: eq_irrelevance. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)