proposition: Lemma nth_enum_ord (n : nat) (i0 : 'I_n) (m : nat) : (m < n)%N -> nth i0 (enum 'I_n) m = m :> nat.
proof: Proof. by move=> lemn; rewrite enum_ord nth_enum_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)