proposition: Lemma congr_cons w1 w2 a : r w1 w2 -> r (a :: w1) (a :: w2).
proof: Proof. Proof using Hcongr. rewrite -[a :: w1]cat1s -[[:: a] ++ w1]cats0 -catA. rewrite -[a :: w2]cat1s -[[:: a] ++ w2]cats0 -catA. exact: Hcongr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK