proposition: Lemma Rank2K i0 (k : 'I_(p_ i0)) : sig2 (Rank k) = cast_ord (congr1 p_ (esym (Rank1K k))) k.
proof: Proof. by apply: val_inj; rewrite /sig2/sig1/Rank/= rankK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)