proposition: Lemma cdiff_pr1' a b: cardinalp a -> natp b -> (a +c b) -c b = a.
proof: Proof. move=> aN bN. have aa: a -c \0c = a by rewrite /cdiff setC_0 (card_card aN). move: b bN; apply:Nat_induction; first by rewrite (csum0r aN) aa. by move => n nN hr; rewrite (csum_nS _ nN) (cdiff_succ (CS_sum2 a n) (CS_nat nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)