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