proposition: Lemma invar_step s : all invar s -> all invar (step s).
proof: Proof. Proof using Hinvar. rewrite /step => /allP H; apply/allP => x. rewrite mem_undup mem_cat => /orP[]; first exact: H. move/flatten_mapP=> [y Hyins Hxy]. by move/(_ _ (H _ Hyins))/allP: Hinvar; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK