proposition: Lemma binz_eq0 (n k : int) : (binomialz n k == 0) = (k < 0) || (0 <= n < k).
proof: Proof. apply/idP/idP=> h. case: (ltrP k 0) => //= hk. - case: (lerP 0 n) => /= hn. apply: contraLR h; rewrite -leNgt; move/(bin_nonneg hk). by rewrite lt0r; case/andP. apply: contraLR h => _. rewrite binNzz; apply: mulf_neq0; first by rewrite expfz_eq0 andbF. suff: 0 < binomialz (k - n - 1) k by rewrite lt0r; case/andP. have hnk : k <= k - n - 1 by lia. by apply: bin_nonneg => //; apply: le_trans hnk. case/orP: h => [h | /andP [h1 h2]]; apply/eqP; first by apply: binz_neg. exact: binz_geq. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics