proposition: Lemma perm_allLtn u v a : perm_eq u v -> allLtn u a -> allLtn v a.
proof: Proof. Proof using. move=> Hperm /allP Hall; apply/allP => X Hx. by apply: Hall; rewrite (perm_mem Hperm). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools