proposition: Lemma rule_rtrans x y : y \in rule x -> rtrans x y.
proof: Proof. Proof using. move=> Hrule; apply/rtransP. by apply: (Rew (l := [:: y])); first rewrite /= Hrule. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK