Proof by working backwards(2)

(2) If n^3 + 5n + 6 is divisible by 3 for some integer n, then (n + 1)^3 + 5(n + 1) + 6 is divisible by 3.

(Scratch work)

(n + 1)^3 + 5(n + 1) + 6 = (n + 1)(n^2 + 2n +1) +5n + 5 + 6
                                     
                                       = n^3 + 2n^2 + n + n^2 + 2n + 1 + 5n + 11

                                       = n^3 + 5n + 6 + 3n^2 + 3n + 6

                                       = n^3 + 5n + 6 + 3(n^2 + n + 2)


Proof. Assume that n^3 + 5n + 6 is divisible by 3 for some integer n. Then

3 | (n^3 + 5n + 6) =>

3 | [(n^3 + 5n + 6) + 3(n^2 +n + 2)] =>

3 | [n^3 + 5n + 6 + 3n^2 + 3n + 6] =>

3| [n^3 + 2n^2 +n + n^2 + 2n + 1 + 5n + 11] =>

3| [(n + 1)(n^2 + 2n + 1) + 5n +5 +6] =>

3| [(n + 1)^3 + 5(n + 1) + 6]

QED

Proof by working backwards(1)

Write clear and complete proofs by working backwards for the following mathematical statement.
(1) The expression x + 9/x >= for all real numbers x > 0.
(Scratch work)

x + 9/x >= 6

x^2 + 9 >= 6x

x^2 - 6x + 9 >= 0

(x - 3)^2 >= 0

Proof. Assume that x is a real number with x > 0. Then notice that

(x -3)^2 >= 0

x^2 - 6x +9 >= 0

x^2 + 9 >= 6x

x + 9/x >= 6x.

QED