proposition: Lemma cdiff_ab_le_a a b: cardinalp a -> (a -c b) <=c a.
proof: Proof. by move => ca; move: (sub_smaller (@sub_setC a b)); rewrite (card_card ca). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)