proposition: Lemma bin_1N (m : int) : 0 <= m -> binomialz (Negz 0) m = (- 1) ^ m.
proof: Proof. by case: m => + // _; elim=> // m ihm; rewrite bin_1N_posz ihm exprSz mulN1r. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics