proposition: Lemma binSz (F : numFieldType) (n k : int) : (k != n + 1) -> (binomialz (n + 1) k)%:~R = (n + 1)%:~R / (n + 1 - k)%:~R * (binomialz n k)%:~R :> F.
proof: Proof. move=> hkn; case: (altP (k =P 0)) hkn => [-> | hk0] hkn. by rewrite !binz0 subr0 divff ?mul1r //; ring_lia. have hk : k = k - 1 + 1 by rewrite -addrA subrr addr0. rewrite hk binzSS; last by rewrite -hk. rewrite binzS; last by rewrite -hk. by field; ring_lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics