proposition: Lemma cardfsD A B : #|` A `\` B| = (#|` A| - #|` A `&` B|)%N.
proof: Proof. by rewrite -(cardfsID B A) addKn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)