proposition: Lemma size_invar (x0 x : word) : szinvar x0 x -> all (szinvar x0) (rule x).
proof: Proof. Proof using Hhom. rewrite /szinvar /= => /eqP <-. exact: Hhom. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK