proposition: Lemma maxL_perm a u b v : perm_eq (a :: u) (b :: v) -> maxL a u = maxL b v.
proof: Proof. Proof using. move/permP => Hperm. have {}Hperm : forall x, (x \in (a :: u)) = (x \in (b :: v)). move=> x; move/(_ (xpred1 x)) : Hperm => Hperm. by apply/idP/idP => /count_memPn H; apply/count_memPn; rewrite ?Hperm // -?Hperm. apply/eqP; rewrite eq_le; apply/andP; split. - move/(_ (maxL a u)) : Hperm; rewrite (in_maxL a u) => /esym Hin. exact: (allP (maxLP b v)). - move/(_ (maxL b v)) : Hperm; rewrite (in_maxL b v) => /esym Hin. exact: (allP (maxLP a u)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools