proposition: Lemma trivIset3 (T : finType) (A B C : {set T}) : [disjoint A & B] -> [disjoint B & C] -> [disjoint A & C] -> trivIset [set A;B;C].
proof: Proof. move => D1 D2 D3. apply/trivIsetP => X Y. rewrite !inE -!orbA. do 2 (case/or3P => /eqP->); try by rewrite ?eqxx // 1?disjoint_sym. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)