proposition: Lemma trivIsetU Q : trivIset Q -> trivIset P -> [disjoint cover Q & cover P] -> trivIset (Q :|: P).
proof: Proof. move => /trivIsetP tQ /trivIsetP tP dQP; apply/trivIsetP => A B. move => /setUP[?|?] /setUP[?|?]; first [exact:tQ|exact:tP|move => _]. by apply: disjointW dQP; rewrite bigcup_sup. by rewrite disjoint_sym; apply: disjointW dQP; rewrite bigcup_sup. Qed.
imports: mathcomp(all_ssreflect)