proposition: Fact join_finerP P Q R : (join_finer P Q <= R)%O = (P <= R)%O && (Q <= R)%O.
proof: Proof. apply/idP/andP=> [Hjoin | [/is_finer_pblockP RA /is_finer_pblockP RB]]. split; apply: (le_trans _ Hjoin); first exact: le_join_finer. by rewrite join_finerC le_join_finer. apply/is_finer_pblockP => x xinS. apply/subsetP=> y /[dup]/mem_pblock_setpart yinS. rewrite (pblock_equivalence_partition (join_finer_equivalence P Q)) //. rewrite {yinS} /join_finer_eq => /closed_connect <-{y}. by rewrite mem_pblock (cover_setpart R). move=> y z /= Hrel; rewrite -!eq_pblock ?(cover_setpart R) //. suff {x xinS} -> : pblock R y = pblock R z by []. move: Hrel=> /orP[zPy | zQy]; apply: same_pblock => //. - have /RA/subsetP := mem_pblock_setpart zPy; apply. by rewrite mem_pblockC. - have /RB/subsetP := mem_pblock_setpart zQy; apply. by rewrite mem_pblockC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition