proposition: Lemma trivIsetP P : reflect {in P &, forall A B, A != B -> [disjoint A & B]} (trivIset P).
proof: Proof. rewrite -[P]set_enum; elim: {P}(enum _) (enum_uniq P) => [_ | A e IHe] /=. by rewrite /trivIset /cover !big_set0 cards0; left=> A; rewrite inE. case/andP; rewrite set_cons -(in_set (fun B => B \in e)) => PA {}/IHe. move: {e}[set x in e] PA => P PA IHP. rewrite /trivIset /cover !big_setU1 //= eq_sym. have:= leq_card_cover P; rewrite -(mono_leqif (leq_add2l #|A|)). move/(leqif_trans (leq_card_setU _ _))->; rewrite disjoints_subset setC_bigcup. case: bigcapsP => [disjA | meetA]; last first. right=> [tI]; case: meetA => B PB; rewrite -disjoints_subset. by rewrite tI ?setU11 ?setU1r //; apply: contraNneq PA => ->. apply: (iffP IHP) => [] tI B C PB PC; last by apply: tI; apply: setU1r. by case/setU1P: PC PB => [->|PC] /setU1P[->|PB]; try by [apply: tI | case/eqP]; first rewrite disjoint_sym; rewrite disjoints_subset disjA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)