proposition: Lemma cast_ord_inj n1 n2 eq_n : injective (@cast_ord n1 n2 eq_n).
proof: Proof. exact: can_inj (cast_ordK eq_n). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)