proposition: Corollary ltperm_invset s t : (s <R t) = (invset s \proper invset t).
proof: Proof. rewrite lt_neqAle leperm_invset properEneq; congr ((negb _) && _). by apply/eqP/eqP => [-> | /invset_inj]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype