proposition: Lemma rewrite_path_trans x y z : rewrite_path x y -> rewrite_path y z -> rewrite_path x z.
proof: Proof. Proof using. move=> [pathxy Hxy Hy] [pathyz Hyz Hz]. apply: (Rew (pathxy ++ pathyz)). - by rewrite cat_path Hxy -Hy Hyz. - by rewrite last_cat -Hy. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK