proposition: Lemma cardinal_setC5 A B: finite_set B -> sub A B -> A =c B -> A = B.
proof: Proof. move => fsB sAB cAB. move: (cardinal_setC4 sAB fsB); rewrite cAB cdiff_nn. by move /card_nonempty /empty_setC /(extensionality sAB). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)