proposition: Lemma cardsDS A B : B \subset A -> #|A :\: B| = (#|A| - #|B|)%N.
proof: Proof. by rewrite cardsD => /setIidPr->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)