proposition: Lemma csum_of_evenP n m: evenp n -> natp m -> (evenp (n +c m) <-> evenp m).
proof: Proof. move => eN mN; split => h; last by apply:csum_of_even. by ex_middle h'; move: (proj2(csum_of_even_odd eN (conj mN h'))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)