proposition: Lemma nth_ord_ltn i n (H : i < n) x0 : nth x0 (enum 'I_n) i = (Ordinal H).
proof: Proof. by apply: val_inj => //=; rewrite nth_enum_ord. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple) mathcomp(finset tuple bigop) tools