proposition: Lemma partitionD1 P D B : partition P D -> B \in P -> partition (P :\ B) (D :\: B).
proof: Proof. case/and3P => /eqP covP trivP set0P SP. by rewrite /partition inE (negbTE set0P) trivIsetD ?coverD1 -?covP ?eqxx ?andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)