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