proposition: Lemma mul_Sm_binom m n : natp n -> natp m -> csucc m *c binom m n = csucc n *c binom (csucc m) (csucc n).
proof: Proof. move => nN mN; move: m mN n nN ; apply: Nat_induction. move => n nN; case: (czero_dichot (CS_nat nN)) => nz. by rewrite nz succ_zero (binom_nn NS0) (binom_nn NS1). rewrite (binom_bad NS0 nN nz) (binom_bad); fprops; last by apply: cltSS. by rewrite !cprod0r. move => m mN Hrec n nN. have smN := (NS_succ mN). case: (czero_dichot (CS_nat nN)) => nz. by rewrite nz (binom0 smN) succ_zero (binom1 (NS_succ smN)) cprodC. move: (cpred_pr nN (nesym (proj2 nz))); set k := cpred n; move => [kN ->]. move: (NS_succ kN) => skN. rewrite (cprod_Sn _ smN) {2} (binomSnSm mN kN) cprodDr (Hrec _ skN) (Hrec _ kN). by rewrite csumCA - (cprod_Sn _ (NS_succ kN)) - cprodDr - (binomSnSm smN skN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)