Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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.
