proposition: Lemma coverD1 S : trivIset P -> S \in P -> cover (P :\ S) = cover P :\: S.
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: mathcomp(all_ssreflect)