proposition: Lemma csum_of_odd a b: oddp a -> oddp b -> evenp (a +c b).
proof: Proof. move => /(oddp_alt) [aN ao] /(oddp_alt) [bN bo]. split; first fprops. by rewrite (crem_sum NS2 card2_nz aN bN) ao bo csum_11 crem_22. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)