proposition: Fact leperm_length s t : s <=R t -> length s <= length t.
proof: Proof. by move/lepermP => [u _ ->]; apply leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype