proposition: Lemma trivIsetU1 A P : {in P, forall B, [disjoint A & B]} -> trivIset P -> set0 \notin P -> trivIset (A |: P) /\ A \notin P.
proof: Proof. move=> tiAP tiP notPset0; split; last first. apply: contra notPset0 => P_A. by have:= tiAP A P_A; rewrite -setI_eq0 setIid => /eqP <-. apply/trivIsetP=> B1 B2 /setU1P[->|PB1] /setU1P[->|PB2]; by [apply: (trivIsetP _ tiP) | rewrite ?eqxx // ?(tiAP, disjoint_sym)]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)