Let n be an integer, and let (L_n) signify the nth Lucas Number.

((L_n)²+(L_n+1)²)² - 5((L_2n+2)*(L_2n)-1) = 0

Prove it!

Excellent!

If you don't mind, please consider this line:

(L_2n)²-3L_2n*L_2n+2+(L_2n+2)² + 5 = 0

and the generalised substitution a^2-3ab+b^2 = -5.

Are they not fully equivalent?

If so, are the remaining lines strictly necessary? I'd be grateful to hear your views, as I by no means claim to be an expert in matters of proof.