proposition: Lemma sub_partition_sub A : partition P D -> A \subset D -> sub_partition A \subset [set B :&: A | B in P].
proof: Proof. move=> partP /subsetP subAD; apply/subsetP => B; case/imsetP => [x xA ->]. have ? : x \in cover P by rewrite (cover_partition partP) subAD. apply/imsetP; exists (pblock P x); first by rewrite pblock_mem. by apply/setP => y; rewrite !inE eq_pblock 1?andbC //; case/and3P: partP. Qed.
imports: mathcomp(all_ssreflect)