proposition: Lemma join_finerE P Q x y : x \in S -> y \in pblock (P `|` Q)%O x = join_finer_eq P Q x y.
proof: Proof. move=> xinS; case/boolP: (y \in S) => [yinS | yninS]. by rewrite -(pblock_equivalence_partition (join_finer_equivalence P Q)). have:= yninS; rewrite -(pblock_notin (P `|` Q)%O) negbK. rewrite mem_pblockC // => /eqP ->. rewrite inE; apply/esym/negbTE. by move: yninS; apply contra; exact: join_finer_eq_in_S. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition