proposition: Lemma partition_partition (T : finType) (D : {set T}) P Q : partition P D -> partition Q P -> partition (cover @: Q) D /\ {in Q &, injective cover}.
proof: Proof. move=> /and3P[/eqP defG tiP notP0] /and3P[/eqP defP tiQ notQ0]. have sQP E: E \in Q -> {subset E <= P}. by move=> Q_E; apply/subsetP; rewrite -defP (bigcup_max E). rewrite /partition cover_imset -(big_trivIset _ tiQ) defP -defG eqxx /= andbC. have{} notQ0: set0 \notin cover @: Q. apply: contra notP0 => /imsetP[E Q_E E0]. have /set0Pn[/= A E_A] := memPn notQ0 E Q_E. congr (_ \in P): (sQP E Q_E A E_A). by apply/eqP; rewrite -subset0 E0 (bigcup_max A). rewrite notQ0; apply: trivIimset => // E F Q_E Q_F. apply: contraR => /pred0Pn[x /andP[/bigcupP[A E_A Ax] /bigcupP[B F_B Bx]]]. rewrite -(def_pblock tiQ Q_E E_A) -(def_pblock tiP _ Ax) ?(sQP E) //. by rewrite -(def_pblock tiQ Q_F F_B) -(def_pblock tiP _ Bx) ?(sQP F). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)