proposition: Lemma sum_nm_times : forall (n m x : nat) (f : nat -> nat), x * sum_nm n m f = sum_nm n m (fun i : nat => x * f i).
proof: Proof. intros n m x f; generalize n; clear n; elim m; simpl in |- *; auto. intros m' Rec n. rewrite <- Rec; auto with arith. ring. Qed.
imports: Coq(Arith ArithRing)