proposition: Lemma partitionU1 P D B : partition P D -> B != set0 -> [disjoint B & D] -> partition (B |: P) (B :|: D).
proof: Proof. case/and3P => /eqP covP trivP set0P BD0 disSD. rewrite /partition !inE (negbTE set0P) orbF [_ == B]eq_sym BD0 andbT. rewrite /cover bigcup_setU /= big_set1 -covP eqxx /=. by move: disSD; rewrite -covP=> /bigcup_disjointP/trivIsetU1 => -[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)