proposition: Lemma ord2P n (m : 'I_n.+2) : ord2_spec m.
proof: Proof. case: (unliftP ord0 m) => [j Hj|/eqP]; last exact: Ord20. case: (unliftP ord_max j) => [i Hi|Hj2]; last apply: Ord2M. * apply: (@Ord2C _ m i). by rewrite Hj Hi lift0 lift_max. * rewrite Hj Hj2. apply/eqP. apply/ord_inj. by rewrite lift0. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)