proposition: Lemma rewrite_path_min (r : rel T) : equivalence_rel r -> (forall x y, y \in rule x -> r x y) -> forall x y, rewrite_path rule x y -> r x y.
proof: Proof. Proof using. rewrite equivalence_relP => [] [Hrefl Htr] Hin x y [l]. elim: l x => [/= x _ -> | l0 l IHl] /=; first exact: Hrefl. move=> x /andP[/Hin Hl0 {}/IHl/[apply] Hl0y]. by rewrite (Htr _ _ Hl0 y). Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK