proposition: Lemma rule_gencongr u v : v \in rule u -> v \in gencongr u.
proof: Proof. Proof using. move=> H; apply rule_rtrans; exact: rule_congrrule. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK