proposition: Lemma perm_allLtnE u v a : perm_eq u v -> allLtn u a = allLtn v a.
proof: Proof. Proof using. move=> H; apply/idP/idP; apply: perm_allLtn; first by []. by rewrite perm_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools