proposition: Theorem Nbinomial_n_1 : forall n, 1 <= n -> Nbinomial n 1 = n.
proof: Proof. induction n. compute. reflexivity. intros. unfold Nbinomial. assert (leb 1 (S n)=true). apply leb_correct. exact H. rewrite H0. unfold Nsimple_binomial. fold Nsimple_binomial. destruct n. compute. reflexivity. assert (Nbinomial (S n) 1=S n). apply IHn. auto with arith. clear IHn. unfold Nbinomial in H1. clear H0. assert (leb 1 (S n)=true). apply leb_correct. auto with arith. rewrite H0 in H1. clear H0. rewrite H1. compute. reflexivity. Qed.
imports: Arith Compare Nfinite_prod Ndiv