proposition: Lemma perm_std u v : is_std u -> perm_eq v u -> is_std v.
proof: Proof. rewrite /is_std => Hperm Heq. rewrite (perm_size Heq); exact: (perm_trans Heq Hperm). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp