proposition: Lemma rtrans_min (r : rel T) : equivalence_rel r -> (forall x y, y \in rule x -> r x y) -> forall x y, rtrans x y -> r x y.
proof: Proof. Proof using. move/rewrite_path_min=> /[apply] H x y /rtransP Hrew; exact: H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK