proposition: Lemma subset_s_trans_s s : {subset s <= trans s}.
proof: Proof. Proof using. apply trans_ind => //= {s}. - by move=> s _ _ H x Hx; exact (H _ (subset_step Hx)). - by move=> s _ tmp _ {tmp} _ x; rewrite mem_undup. - by move=> s _ tmp _ {tmp} x; rewrite mem_undup. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK