# Induction COQ Question

Just practicing some induction 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,
sum_n_random n * 30 + n * (n + 1) * (2 * n + 1) = n * (n + 1) * (2 * n + 1) * (3 * n * n + 3 * n).
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
Commented May 15, 2023 at 21:28
• Are you trying to get solution to some class exercises?
– Lolo
Commented May 15, 2023 at 23:43
• I think editing a question to ask another question is not in the idea of stack exchange.....
– Lolo
Commented May 15, 2023 at 23:51
• Yep but you want other people to be able to keep track of what is going on.too....
– Lolo
Commented May 15, 2023 at 23:55
• Anyway if you are a beginner in Coq and you've managed to solve the inital question. Congrat!
– Lolo
Commented May 15, 2023 at 23:56

It depends on what you are allowed to use. But since you use ring, this induction principle might come handy:

    Lemma crossinduction (a b: nat -> nat):
a 0 = b 0 -> (forall n, a n + b (S n) = b n + a (S n)) ->
forall n, a n = b n.
Proof.
intros base step n. induction n.
- exact base.
- specialize (step n). rewrite IHn in step. apply cancel in step.
symmetry. exact step.
Qed.