proposition: Lemma nat_cast_ord: forall n m (H: n = m) (i: 'I_n), nat_of_ord (cast_ord H i) = i.
proof: Proof. move=> n m H i. by case: m / H. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations