proposition: Lemma card_sub_partition A : partition P D -> A \subset D -> #|sub_partition A| <= #|P|.
proof: Proof. move=> partP subAD; apply: leq_trans (leq_imset_card (fun B => B :&: A) _). apply: subset_leq_card. exact: sub_partition_sub. Qed.
imports: mathcomp(all_ssreflect)