proposition: Lemma cardsC1 a : #|[set~ a]| = #|T|.-1.
proof: Proof. by rewrite -(cardC1 a); apply: eq_card=> x; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)