proposition: Lemma rtransP x y : reflect (rewrite_path rule y x) (rtrans y x).
proof: Proof. Proof using. rewrite /rtrans /rclass. apply: (iffP idP). - move/transP => H. have: (all (invar inv y) [:: y]). apply/allP=> z; rewrite mem_seq1 => /eqP ->. exact: Hinvar_refl. by move/H => [z] []; rewrite mem_seq1 => /eqP ->. - move=> H; apply/transP. + apply/allP=> x0; rewrite mem_seq1 => /eqP ->. exact: Hinvar_refl. + by exists y; rewrite mem_seq1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK