proposition: Fact suppermP s t w : s <=R w -> t <=R w -> (supperm s t) <=R w.
proof: Proof. rewrite !leperm_invset invset_supperm => Hsw Htw; apply tclosure_sub. - by rewrite subUset Hsw Htw. - by move: (invsetP w) => []. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype