proposition: Lemma le_join_finer P Q : (P <= join_finer P Q)%O.
proof: Proof. apply/is_finer_pblockP=> x xinS; apply/subsetP => y yPx. have yinS := mem_pblock_setpart yPx. rewrite (pblock_equivalence_partition (join_finer_equivalence P Q)) //. by rewrite /join_finer_eq /=; apply: connect1; rewrite /= yPx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition