proposition: Lemma binNzz (n m : int) : binomialz n m = (- 1) ^ m * binomialz (m - n - 1) m.
proof: Proof. wlog: m n / n <= 0. case: n => n; last exact. case: m => m; last by rewrite !binz_neg // mulr0. rewrite binz_nat_nat -addrA -opprB opprK. case: (ltnP n m) => hnm hwlog. by rewrite bin_small // subzn // binz_nat_nat bin_small ?mulr0; lia. have {}hnm : Posz m - Posz n.+1 <= 0 by rewrite subr_le0; apply/leqW/hnm. rewrite [in RHS]hwlog // subKr addrAC subrr add0r. by rewrite binz_nat_nat mulrA /exprz /= -exprMn mulrNN mul1r expr1n mul1r. case: m => m; last by rewrite !binz_neg // mulr0. case: n => [n | n _]. case: n => [_ | //]; case:m => [ | m]; first by rewrite !binz0. by rewrite bin0z // subr0 subzSS subr0 binz_nat_nat bin_small // mulr0. rewrite [in RHS]NegzE opprK -addrA subzSS subr0. move: {2}(m + n)%N (leqnn (m + n)) => k; elim: k n m => [n m|k ihk n m hnm]. by rewrite leqn0 addn_eq0; case/andP => /eqP -> /eqP ->; rewrite !binz0. case: m hnm => [ | m] hnm //; case: n hnm => [ | n] hnm. by rewrite bin_1N_posz {}ihk // !addr0 !binz_on_diag /= !mulr1 exprSz mulN1r. rewrite bin_negz_posz ihk; last by move: hnm; rewrite addnS. rewrite ihk; last by move: hnm; rewrite addSn. rewrite exprSzr -!mulrA !mulN1r -mulrBr; congr (_ * _); rewrite -opprD. rewrite -!PoszD ![(m.+1 + _)%N]addSn [(_ + n.+1)%N]addnS -[(m + n).+2]addn1. by rewrite -[m.+1]addn1 !PoszD Pascal_z. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics