proposition: Lemma perm_invar (x0 x : word) : perm_eq x0 x -> all (perm_eq x0) (rule x).
proof: Proof. Proof using Hmulthom. move: perm_trans; rewrite /transitive => Ptrans. move=> H; apply/allP => x1 Hx1; apply: (@Ptrans _ x _ _ H). by move/(_ x)/allP : Hmulthom; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK