proposition: Lemma Nbinomial_pascal: forall n k, k <= n -> Nbinomial n k + Nbinomial n (S k) = Nbinomial (S n) (S k).
proof: Proof. intros. assert (S k<=n -> Nbinomial n k + Nbinomial n (S k) = Nbinomial (S n) (S k)). intro. apply Nbinomial_pascal'. exact H0. assert (k=n -> Nbinomial n k + Nbinomial n (S k) = Nbinomial (S n) (S k)). intro. rewrite H1. assert (Nbinomial n (S n)=0). apply Nbinomial_outside. auto with arith. rewrite H2. clear H2. rewrite Nbinomial_diag. rewrite Nbinomial_diag. auto with arith. apply le_le_S_eq in H. elim H. exact H0. exact H1. Qed.
imports: Arith Compare Nfinite_prod Ndiv