proposition: Lemma binzSS_weak (F : numFieldType) (n k : int) : 0 <= n -> k + 1 != 0 -> (binomialz (n + 1) (k + 1))%:~R = (n + 1)%:~R / (k + 1)%:~R * (binomialz n k)%:~R :> F.
proof: Proof. case: n k => [] // n [k|[|k]] // _ _; last by rewrite !binz_neg // mulr0. rewrite -!PoszD !addn1 !binz_nat_nat mulrAC. apply: canRL (mulfK _) _; rewrite ?intr_eq0 //. by rewrite -!intrM -!PoszM mul_bin_diag mulnC. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics