proposition: Lemma leq_card_cover P : #|cover P| <= \sum_(A in P) #|A| ?= iff trivIset P.
proof: Proof. split; last exact: eq_sym. rewrite /cover; elim/big_rec2: _ => [|A n U _ leUn]; first by rewrite cards0. by rewrite (leq_trans (leq_card_setU A U).1) ?leq_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)