proposition: Lemma partitionU1 S : partition P D -> S != set0 -> [disjoint S & D] -> partition (S |: P) (S :|: D).
proof: Proof. case/and3P => /eqP covP trivP set0P SD0 disSD. rewrite /partition !inE (negbTE set0P) orbF [_ == S]eq_sym SD0 andbT. rewrite /cover bigcup_setU big_set1 -covP eqxx /=. by move: disSD; rewrite -covP=> /bigcup_disjointP/trivIsetU1 => -[]. Qed.
imports: mathcomp(all_ssreflect)