proposition: Lemma prod_nm_f : forall (n m : nat) (f : nat -> nat), prod_nm n (S m) f = prod_nm n m f * f (n + S m).
proof: Proof. intros n m; generalize n; clear n; elim m; simpl in |- *; auto with arith. intros n f; repeat rewrite (fun x y => Nat.add_comm x (S y)); simpl in |- *; auto. intros n Rec m' f. rewrite Rec; repeat (rewrite (Nat.add_comm m'); simpl in |- *); auto with arith. Qed.
imports: Coq(Arith ArithRing) Bertrand(Power)