proposition: Theorem arith_sum : forall a b n, 2 * sum (fun i => a + i * b) n = S n * (2 * a + n * b).
proof: Proof. intros a b n. induction n; simpl; ring_simplify; auto. try change (BinNat.N.to_nat 2) with 2. try change (BinNat.N.to_nat 3) with 3. try change (BinNat.N.to_nat 4) with 4. rewrite IHn; ring. Qed.
imports: Arith