proposition: Lemma nth_sizeu u v a b : nth inh (u ++ [:: a; b] ++ v) (size u) = a.
proof: Proof. Proof using. by rewrite nth_cat ltnn subnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp