proposition: Fact supperm_is_join x y z : (supperm x y <=R z) = (x <=R z) && (y <=R z).
proof: Proof. apply/idP/idP => [leinf | /andP[xley xlez]]; last exact: suppermP. by apply/andP; split; apply: (le_trans _ leinf); [apply: suppermPr | apply: suppermPl]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype