proposition: Lemma nth_sizeu2 u v a b c : nth inh (u ++ [:: a; b; c] ++ v) (size u).+2 = c.
proof: Proof. Proof using. rewrite nth_cat ltnNge (leq_trans (leqnSn _) (leqnSn _)) /=. by rewrite -add1n -[(size u).+1]add1n addnA addn1 (addnK (size u) 2). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp