How do I prove this theorem with induction in COQ

Question

Require Import Arith.

Fixpoint sum_n n :=
  match n with
  |  0 => 0
  | S p => p + sum_n p
  end.

Fixpoint sum_n2 n :=
  match n with
  |  0 => 0
  | S p => n * n + sum_n2 p
  end.

Fixpoint sum_n3 n :=
  match n with
  |  0 => 0
  | S p => p * p * p + sum_n3 p
  end.

Fixpoint sum_odd_n (n:nat) : nat :=
  match n with
  |  0 => 0
  | S p => 1 + 2 * p + sum_odd_n p
  end.

(* You may use the following lemma. *)

Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n.
Proof.
  induction n; simpl; try reflexivity.
  replace (S (n + n * S n)) with (S (n + n * n + n)) by ring;
    rewrite <- IHn; ring.
Qed.

Question 1 :

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1).
Proof.
 intro. induction n; simpl sum_n2.
 ring.
 ring_simplify. 
 rewrite IHn. 
 ring.
Qed.

Question 2 :

Lemma sum_cube_p : forall n, sum_n3 n = (sum_n n) * (sum_n n).
Proof.
 intros. induction n; simpl sum_n3.


Qed.

and

Question 3:

Lemma odd_sum : forall n, sum_odd_n n = n * n.
Proof.
 
Qed.

Answer 1

You can take advantage of the ring tactic that can prove equality modulo associativity and commutativity

Require Import Arith.

Fixpoint sum_n n :=
  match n with
  |  0 => 0
  | S p => n + sum_n p
  end.

Fixpoint sum_n2 n :=
  match n with
  |  0 => 0
  | S p => n * n + sum_n2 p
  end.

Fixpoint sum_n3 n :=
  match n with
  |  0 => 0
  | S p => n * n * n + sum_n3 p
  end.

Fixpoint sum_odd_n (n:nat) : nat :=
  match n with
  |  0 => 0
  | S p => 1 + 2 * p + sum_odd_n p
  end.

Lemma sum_n_p : forall n, 2 * sum_n n = n * (n + 1).
Proof.
now induction n as [|n IH]; simpl; try ring [IH].
Qed.

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1).
Proof.
 now induction n as [|n IH]; simpl; try ring [IH].
Qed.

Lemma sum_cube_p : forall n, sum_n3 n = (sum_n n) * (sum_n n).
Proof.
intro n.
apply (Nat.mul_cancel_l _ _ 4); auto with arith.
now induction n as [|n IH]; simpl; try ring[IH (sum_n_p n)].
Qed.

Lemma odd_sum : forall n, sum_odd_n n = n * n.
Proof.
now induction n as [|n IH]; simpl; try ring [IH].
Qed.