proposition: Lemma binomSnSm n m: natp n -> natp m -> binom (csucc n) (csucc m) = (binom n (csucc m)) +c (binom n m).
proof: Proof. move=> nN mN. have snz := (@succ_nz m); have smN:= NS_succ mN. rewrite /binom /variant induction_terms // LgV//. Ytac0; rewrite cpred_pr1 //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)