proposition: Lemma binom_rec1 n k: natp n -> k <=c n -> (n -c k) *c (binom n k) = (csucc k) *c binom n (csucc k).
proof: Proof. move => nN lkn; move: (NS_diff k nN) (NS_le_nat lkn nN) => ha hb. by rewrite - {2 3} (cdiff_pr lkn) csumC mul_Sm_binom_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)