proposition: Lemma gencongr_equiv : equivalence_rel gencongr.
proof: Proof. Proof using Hsym. apply: equiv_rtrans => x y; exact: congrrule_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK