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