proposition: Lemma inord_inj n m : n <= m -> injective (@inord m \o @nat_of_ord n.+1).
proof: Proof. move => Hnm k k' /= /(f_equal (@nat_of_ord _)) E. apply/ord_inj. rewrite !inordK // in E; exact: leq_trans (ltn_ord _) _. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)