proposition: Lemma cardfsD1 a A : #|` A| = (a \in A) + #|` A `\ a|.
proof: Proof. rewrite -(cardfsID [fset a]) fsetI1 (fun_if (fun A => #|` A|)). by rewrite cardfs0 cardfs1; case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)