proposition: Theorem prod_nm_split : forall (f : nat -> nat) (p q r : nat), r < q -> prod_nm p q f = prod_nm p r f * prod_nm (1 + (p + r)) (q - (1 + r)) f.
proof: Proof. intros f p q; elim q. intros r H; inversion H; simpl in |- *. intros n H r H0; inversion H0. rewrite prod_nm_f. rewrite Nat.sub_diag; rewrite <- plus_n_Sm; simpl in |- *; auto. rewrite prod_nm_f; rewrite (H r); auto with arith. rewrite Nat.sub_succ_l; auto with arith. rewrite prod_nm_f; auto with arith. replace (1 + (p + r) + S (n - (1 + r))) with (p + S n); auto with arith. rewrite <- Nat.sub_succ_l; auto with arith. replace (1 + (p + r) + (S n - (1 + r))) with (p + (1 + r + (S n - (1 + r)))); [ idtac | ring ]. rewrite (Nat.add_comm (1 + r)), Nat.sub_add; auto with arith. Qed.
imports: Coq(Arith ArithRing) Bertrand(Power)