proposition: Lemma Nbinomial_pascal': forall n k, S k <= n -> Nbinomial n k + Nbinomial n (S k) = Nbinomial (S n) (S k).
proof: Proof. intros. unfold Nbinomial. assert (leb k n=true). apply leb_correct. auto with arith. assert (leb (S k) (S n)=true). apply leb_correct. auto with arith. assert (leb (S k) n=true). apply leb_correct. auto with arith. rewrite H0. clear H0. rewrite H1. clear H1. rewrite H2. clear H2. unfold Nsimple_binomial. fold Nsimple_binomial. reflexivity. Qed.
imports: Arith Compare Nfinite_prod Ndiv