proposition: Theorem prod_nm_c : forall c p q : nat, prod_nm p q (fun x => c) = power c (S q).
proof: Proof. intros c p q; generalize p; elim q; clear p q; simpl in |- *; auto with arith. Qed.
imports: Coq(Arith ArithRing) Bertrand(Power)