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