proposition: Lemma leq_card_fcover P : ((#|` fcover P|)%fset <= \sum_(A <- P) #|`A| ?= iff trivIfset P)%N.
proof: Proof. split; last exact: eq_sym. rewrite /fcover; elim/big_rec2: _ => [|A n U _ leUn]; first by rewrite cardfs0. by rewrite (leq_trans (leq_card_fsetU A U).1) ?leq_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)