proposition: Lemma trivIfsetP P : reflect {in P &, forall A B, A != B -> [disjoint A & B]%fset} (trivIfset P).
proof: Proof. have [l Pl ul] : {l | enum_fset P =i l & uniq l} by exists (enum_fset P). elim: l P Pl ul => [P P0 _|A e ih P PAe] /=. rewrite /trivIfset /fcover. have -> : P = fset0 by apply/fsetP => i; rewrite P0 !inE. rewrite !big_seq_fset0 cardfs0 eqxx. by left => x y; rewrite in_fset0. have {PAe} -> : P = [fset x | x in A :: e]%fset. by apply/fsetP => i; rewrite !inE /= PAe inE. move=> {P} /andP[]; rewrite fset_cons => Ae ue. set E := [fset x | x in e]%fset; have Ee : E =i e by move=> x; rewrite !inE. rewrite -Ee in Ae; move: (ih _ Ee ue) => {}ih. rewrite /trivIfset /fcover !big_fsetU1 // eq_sym. have := leq_card_fcover E; rewrite -(mono_leqif (leq_add2l #|` A|)). move/(leqif_trans (leq_card_fsetU _ _)) => /= ->. have [dAcE|dAcE]/= := boolP [disjoint A & fcover E]%fset; last first. right=> tI; move/negP : dAcE; apply. rewrite -fsetI_eq0; apply/eqP/fsetP => t; apply/idP/idP => //; apply/negP. rewrite inE => /andP[tA]. rewrite /cover => /bigfcupP[/= B]; rewrite andbT => BE tB. have AB : A != B by apply: contra Ae => /eqP ->. move: (tI A B). rewrite 2!inE eqxx /= => /(_ isT); rewrite 2!inE BE orbT => /(_ isT AB). by move/disjoint_fsetI0 => /fsetP /(_ t); rewrite inE tA tB inE. apply: (iffP ih) => [tI B C|tI B C PB PC]; last first. by apply: tI; rewrite !inE /= -Ee ?(PB,PC) orbT. rewrite 2!inE => /orP[/eqP->{B}|BE]. rewrite 2!inE => /orP[/eqP->|{tI}]; first by rewrite eqxx. move: dAcE; rewrite -fsetI_eq0 => /eqP AE0 CE AC. rewrite -fsetI_eq0; apply/eqP/fsetP => t; apply/idP/idP; apply/negP. rewrite inE => /andP[tA tC]. move/fsetP : AE0 => /(_ t); rewrite !inE tA /= => /negbT/negP; apply. by apply/bigfcupP; exists C => //; rewrite CE. rewrite 2!inE => /orP[/eqP-> BA|]; last exact: tI. rewrite -fsetI_eq0; apply/eqP/fsetP => t; apply/idP/idP; apply/negP. rewrite inE => /andP[tB tA]; move: dAcE. rewrite -fsetI_eq0 => /eqP/fsetP/(_ t); rewrite !inE tA /= => /negP; apply. by apply/bigfcupP; exists B => //; rewrite BE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)