proposition: Lemma ltperm_length s t : s <R t -> length s < length t.
proof: Proof. move=> ltst. have:= leperm_length (ltW ltst); rewrite leq_eqVlt => /orP[/eqP | //]. move/(leperm_lengthE (ltW ltst)) => Habs. by rewrite Habs ltxx in ltst. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype