proposition: Lemma gencongr_invar u v : gencongr u v-> invar inv u v.
proof: Proof. Proof using. move: v; apply rtrans_ind; first exact: Hinvar_refl. by move=> v w /congrrule_invar /allP; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK