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