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