proposition: Lemma cardfsU1 a A : #|` a |` A| = (a \notin A) + #|` A|.
proof: Proof. have [aA|aNA] := boolP (a \in A); first by rewrite mem_fset1U. rewrite cardfsU -addnBA ?fsubset_leq_card // fsetIC -cardfsD. by rewrite mem_fsetD1 // cardfs1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)