proposition: Lemma perm_join_meetE s t : s /\R t = maxperm * (maxperm * s \/R maxperm * t).
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) permcomp tools permuted combclass congr presentSn ordtype