The proof is a bit clumsy because you don't have proper
subtraction in nat. One way to go is to suppose first that n
is not zero.
Lemma randompractice : forall n : nat,
sum_n_random n * 30 + n * (n + 1) * (2 * n + 1) = n * (n + 1) * (2 * n + 1) * (3 * n * n + 3 * n).
Proof.
destruct n as [|n]; [trivial|].
assert (H : sum_n_random (S n) * 30 =
S n * (S n + 1) * (2 * S n + 1) * (3 * S n * S n + 3 * n + 2));
[|rewrite H; ring].
induction n as [|n IH]; [trivial|].
replace (sum_n_random (S (S n)) * 30) with
((S (S n)) * (S (S n)) * (S (S n)) * (S (S n)) * 30
+ sum_n_random (S n) * 30) by (simpl; ring).
rewrite IH; ring.
Qed.