proposition: Lemma Nsimple_binomial_outside : forall n m, n < m -> Nsimple_binomial n m = 0.
proof: Proof. induction n. intros. compute. destruct m. apply Nat.lt_irrefl in H. contradiction. reflexivity. intros. unfold Nsimple_binomial. fold Nsimple_binomial. destruct m. apply Nat.nlt_0_r in H. contradiction. assert (n<m). auto with arith. rewrite IHn. simpl. assert (n<S m). auto with arith. apply IHn. auto. auto. Qed.
imports: Arith Compare Nfinite_prod Ndiv