proposition: Lemma binz_nat_nat (n m : nat) : binomialz (Posz n) (Posz m) = 'C(n, m).
proof: Proof. elim: n m => [ | n Hn] [ | n0] //. rewrite -[in LHS](addn1 n) -[in LHS](addn1 n0) 2!PoszD Pascal_z binS. by rewrite !Hn addn1 PoszD. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics