proposition: Lemma coverD1 P B : trivIset P -> B \in P -> cover (P :\ B) = cover P :\: B.
proof: Proof. move/trivIsetP => tP SP; apply/setP => x; rewrite inE. apply/bigcupP/idP => [[A /setD1P [ADS AP] xA]|/andP[xNS /bigcupP[A AP xA]]]. by rewrite (disjointFr (tP _ _ _ _ ADS)) //=; apply/bigcupP; exists A. by exists A; rewrite // !inE AP andbT; apply: contraNneq xNS => <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)