proposition: Lemma prod_nm_mult : forall (n m : nat) (f g : nat -> nat), prod_nm n m f * prod_nm n m g = prod_nm n m (fun i : nat => f i * g i).
proof: Proof. intros n m f g; generalize n; clear n; elim m; simpl in |- *; auto. intros m' Rec n. rewrite <- Rec. ring. Qed.
imports: Coq(Arith ArithRing) Bertrand(Power)