proposition: Lemma ord2PM n : ord2P (@ord_max n.+1) = Ord2M (eqxx _).
proof: Proof. case: (ord2P (@ord_max n.+1)) => //= [H|i Hi]. - apply: f_equal. exact: eq_irrelevance. - move: (ltn_ord i). move: (Hi) => Hi2. move: Hi => [] ->. by rewrite ltnn. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)