proposition: Lemma cdiff_pr5 a b c: cardinalp a -> cardinalp b -> natp c -> (a +c c) -c (b +c c) = a -c b.
proof: Proof. move => ca cb cN;move: c cN; apply: Nat_induction. rewrite !csum0r //. move => n nN Hrec; rewrite (csum_nS _ nN) (csum_nS _ nN) cdiff_succ //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)