proposition: Lemma Pascal_z (n m : int) : binomialz (n + 1) (m + 1) = binomialz n (m + 1) + binomialz n m.
proof: Proof. case: m => m; case: n => n /=; rewrite -?[Posz n + 1]PoszD -?[Posz m + 1]PoszD ?addn1. - by rewrite bin_posz_posz addrC. - case: n => [ | n] //=; first by rewrite bin_1N_posz addNr bin0z. by rewrite bin_negz_posz -addrA addNr addr0 NegzE addrC subzSS add0r -NegzE. - case: m => [ | m]; first by rewrite subrr /= addr0. by rewrite NegzE addrC subzSS add0r -NegzE; case: m => [ | m]. - case: m => [ | m]; last by rewrite !binz_neg. by rewrite !binz0 binz_neg. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics