proposition: Lemma cardsD1 a A : #|A| = (a \in A) + #|A :\ a|.
proof: Proof. by rewrite (cardD1 a); congr (_ + _); apply: eq_card => x; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)