proposition: Lemma perm_allLeq u v a : perm_eq u v -> allLeq u a -> allLeq v a.
proof: Proof. Proof using. move=> Hperm /allLeqP; rewrite (maxL_perm (b := a) (v := v)). - by move=> Hall; apply/allLeqP. - by rewrite perm_cons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools