proposition: Lemma binzSS (F : numFieldType) (n k : int) : k + 1 != 0 -> (binomialz (n + 1) (k + 1))%:~R = (n + 1)%:~R / (k + 1)%:~R * (binomialz n k)%:~R :> F.
proof: Proof. case: n => n; first exact: binzSS_weak. case: k => [k|[|k]] // _; last by rewrite !binz_neg // !mulr0. rewrite mulrAC; apply: (canRL (mulfK _)); first by ring_lia. rewrite [LHS]mulrC [in LHS]binNzz [in RHS]binNzz !rmorphM /=. rewrite opprD addrACA subrr addr0 mulrCA binzS_weak //; [|lia..]. by rewrite -PoszD addn1 exprSz; field; ring_lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics