proposition: Lemma congr_catl u1 u2 v : r u1 u2 -> r (u1 ++ v) (u2 ++ v).
proof: Proof. Proof using Hcongr. by rewrite -[u1 ++ v]cat0s -[u2 ++ v]cat0s; exact: Hcongr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK