proposition: Lemma csum_of_even a b: evenp a -> evenp b -> evenp (a +c b).
proof: Proof. move => [aN ae][bN be]; split; first by fprops. by rewrite (crem_sum NS2 card2_nz aN bN) ae be (csum0r CS0) crem_02. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)