proposition: Theorem equiv_rtrans : equivalence_rel rtrans.
proof: Proof. Proof using Hsym. rewrite equivalence_relP; split. - rewrite /reflexive /rtrans /rclass => x. by apply: subset_s_trans_s; rewrite mem_seq1. - rewrite /left_transitive => x y Hrxy z. apply/idP/idP; move: Hrxy. + move=> /rtransP Hryx /rtransP Hrzx; apply/rtransP. by move/(rewrite_path_sym Hsym) : Hryx => /rewrite_path_trans/(_ Hrzx). + move=> /rtransP Hryx /rtransP Hrzy; apply/rtransP. exact: (rewrite_path_trans (y := y)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK