proposition: Lemma ord2PC n {i : 'I_n.+2} {i' : 'I_n} (p : i'.+1 = i) : ord2P i = Ord2C p.
proof: Proof. case: (ord2P i) => [Hi|Hi|j' p']. - exfalso. move/eqP: Hi => Hi. by rewrite Hi in p. - exfalso. move:Hi. apply/negP. apply: contra_eqN p => /eqP->. rewrite eqn_leq negb_and -[~~ (ord_max <= _)]ltnNge [_.+1 < _](_ : _ = true) ?orbT //. exact: leq_ltn_trans (ltn_ord _) _. - have ?: i' = j'. apply: ord_inj. apply/eqP. by rewrite -eqSS p p'. subst. by rewrite (eq_irrelevance p p'). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)