proposition: Lemma invar_rewrite_path x y : invar x -> rewrite_path x y -> invar y.
proof: Proof. Proof using Hinvar. move=> Hx [l]. elim: l x Hx => [x Hx _ -> // | l0 l IHl] x Hx /= /andP[Hrule /IHl]; apply. by move/(_ _ Hx)/allP: Hinvar; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK