proposition: Lemma DE_eq6_solution (x y:int): (x^+2 - x*y - x - y^+2 == 0) <-> exists n, [\/ y = (fib n.*2 * fib n.*2.+1)%N /\ x = (fib n.*2.+1 ^ 2)%N, y = (fib n.*2 * fib n.*2.+1)%N /\ x = -((fib n.*2 ^ 2)%N:int), y = -((fib n.*2.+2 * fib n.*2.+1)%N:int) /\ x = (fib n.*2.+1 ^ 2)%N | y = -((fib n.*2.+2 * fib n.*2.+1)%N:int) /\ x = -((fib n.*2.+2^2)%N:int) ].
proof: Proof. split. move => h. case: (lerP 0 y) => yp. move: (DE_eq6_pos yp h) => [n [ha hb]]; exists n. by case: hb; [ constructor 1 | constructor 2]. move: (DE_eq6_neg yp h) => [n [ha hb]]; exists n. by case: hb; [ constructor 3 | constructor 4]. have hu (a:nat): (a%:Z)^+2 = (a^2)%:Z by []. rewrite /DE_eq6; move => [n]; move: (DE_eq6_sol n) => [ea eb ec ed]. case; move => [-> ->]. + rewrite addrAC - addrA addrAC addrA hu ea PoszD hu addrK PoszD addrK. by rewrite PoszM subrr. + by rewrite - mulNr opprK sqrrN ! hu -PoszM -PoszD eb subrr. + by rewrite sqrrN -mulrN opprK ! hu -PoszM -PoszD ec addnC PoszD addrK subrr. + rewrite !sqrrN mulrN !opprK mulNr - addrA addrACA - opprD !hu. by rewrite - PoszM -PoszD ed -PoszD subrr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)