proposition: Lemma partitionD1 S : partition P D -> S \in P -> partition (P :\ S) (D :\: S).
proof: Proof. case/and3P => /eqP covP trivP set0P SP. by rewrite /partition inE (negbTE set0P) trivIsetD ?coverD1 -?covP ?eqxx ?andbF. Qed.
imports: mathcomp(all_ssreflect)