proposition: Lemma DE_eq6_sol n (x := fib n.*2.+1) (y := fib n.*2)(z := fib n.*2.+2): [/\ (x ^ 2)^2 = (x ^ 2)*(y * x) + (x ^ 2) + (y * x)^2, (y ^ 2)^2 + (y ^ 2)*(y * x) + (y ^ 2) = (y * x)^2, (x ^ 2)^2 + (x ^ 2)*(z * x) = (x ^ 2) + (z * x)^2 & (z ^ 2)^2 + (z ^ 2) = (z ^ 2)*(z * x) + (z * x)^2] %N.
proof: Proof. split. + rewrite (mulnC y) expnMn -mulnSr -mulnDr addnC - (addn1 (x* y)%N) addnA. by rewrite -(DE1_sol n) mulnn. + rewrite -addnA -mulnSr -mulnn -mulnDr expnMn. by rewrite (mulnC y) - (addn1 (x* y)%N) (DE1_sol n) addnA. + by rewrite -mulnn -mulnDr - (DE2_sol n) mulnDr muln1 addnC mulnC expnMn. + by rewrite -mulnn -mulnSr expnMn -mulnDr (addnC (z*x)%N) -DE2_sol addn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)