proposition: Lemma binzS_weak (F : numFieldType) (n k : int) : n >= 0 -> k + 1 != 0 -> (binomialz n (k + 1))%:~R = (n - k)%:~R / (k + 1)%:~R * (binomialz n k)%:~R :> F.
proof: Proof. case: n k => [] // n [k|[|k]] // _ _; last by rewrite !binz_neg // mulr0. have ->: (Posz n - Posz k) = ((Posz n + 1) - (Posz k + 1)) by ring. rewrite rmorphB !mulrBl /= -binzSS_weak //; last lia. rewrite divff ?mul1r; last ring_lia. by rewrite Pascal_z rmorphD addrK. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics