proposition: Lemma Nbinomial_0 : forall n, Nbinomial n 0 = 1.
proof: Proof. destruct n. compute. reflexivity. unfold Nbinomial. assert (leb 0 (S n)=true). apply leb_correct. auto with arith. rewrite H. clear H. unfold Nsimple_binomial. reflexivity. Qed.
imports: Arith Compare Nfinite_prod Ndiv