# inductive COQ concern

Just practicing some inductive proofs and was wondering what would be the fastest and most effective way to solve this proof and proofs similar to this?

Lemma randompractice : forall n : nat,
random_n n * 30 + n * (n + 1) *n * 30n * 30 + n
* (n + 1) *n * 30 + n * (n + 1) *n * 30 + n * (n + 1)
* + n * (n + 1) * (2 * n + 1) = n * (n + 1) *
2 * n + 1) * (3 * n * n + 3 * n).n * 30 + n * (n + 1) *
Proof.


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.

• you really did this! Impressive!!
– Lolo
May 15 at 21:28
• Are you trying to get solution to some class exercises?
– Lolo
May 15 at 23:43
• I think editing a question to ask another question is not in the idea of stack exchange.....
– Lolo
May 15 at 23:51
• Yep but you want other people to be able to keep track of what is going on.too....
– Lolo
May 15 at 23:55
• Anyway if you are a beginner in Coq and you've managed to solve the inital question. Congrat!
– Lolo
May 15 at 23:56