proposition: Lemma perm_invar_congr u (a b1 b2 c : word) : invar invcont_perm b1 b2 -> invar invcont_perm u (a ++ b1 ++ c) -> invar invcont_perm u (a ++ b2 ++ c).
proof: Proof. Proof using. by rewrite /= => Hb1b2 /permPl ->; rewrite perm_cat2l perm_cat2r. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK