proposition: Lemma pairwise_eq : antisymmetric r -> forall xs ys, pairwise r xs -> pairwise r ys -> perm_eq xs ys -> xs = ys.
proof: Proof. move=> r_asym; elim=> [|x xs IHxs] [|y ys] //=; try by move=> ? ? /perm_size. move=> /andP [r_x_xs pxs] /andP [r_y_ys pys] eq_xs_ys. move: (mem_head y ys) (mem_head x xs). rewrite -(perm_mem eq_xs_ys) [x \in _](perm_mem eq_xs_ys) !inE. case: eqVneq eq_xs_ys => /= [->|ne_xy] eq_xs_ys ys_x xs_y. by rewrite (IHxs ys) // -(perm_cons x). by case/eqP: ne_xy; apply: r_asym; rewrite (allP r_x_xs) ?(allP r_y_ys). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)