proposition: Lemma lucas_is_square n x: (lucas n) == x^2 = ((n==1) &&(x==1 )) || (n==3) && (x==2).
proof: Proof. apply/idP/idP; last by case/orP => /andP[/eqP -> /eqP ->]. have Hb:[\/ x ^2 == 0 %[mod 8], (x ^2 == 1 %[mod 8]) | x ^2 == 4 %[mod 8] ]. have H a b: (a.*2.*2 +b)^2 = b ^2 %[mod 8]. rewrite sqrnD addnAC -2!mul2n mulnA expnMn -[(2 * 2) ^ 2]/(8 * 2). by rewrite 2! (mulnA 2) -[2*(2*2)]/8 - 2!mulnA - mulnDr mulnC modnMDl. case:(odd_dichot x); case:(odd_dichot x./2)=> -> ->; set y := x./2./2. - by constructor 2; rewrite doubleS - addn3 H. - by constructor 2; rewrite - addn1 H. - by constructor 3; rewrite doubleS - addn2 H. - by constructor 1; rewrite - (addn0 (y.*2).*2) H. have Ha a b: lucas (12 * a + b) = lucas b %[mod 8]. suff Hc c: lucas (12 + c) = lucas c %[mod 8]. by elim: a => // a hr; rewrite mulnS -addnA Hc hr. case:c => // c. rewrite addnS addnC lucas_add fibSS addnC mulnDr addnA -mulnDl. rewrite -[fib 12]/(18 *8) mulnA modnMDl -[fib 11]/(11*8 +1). by rewrite mulnDr mulnA modnMDl muln1. move: (divn_eq n 12); set a := n %/ 12; set b := n %% 12 => nv. move => eq1; case:(odd_dichot n) => eq2; last first. move:(lucas_square n./2); rewrite - eq2 (eqP eq1);case: odd. move => h; case:(ltnP (x^2) 2) => sa. move: h; rewrite (eqP (ltnW sa)) => sb. by move: (lucas_gt0 n./2); rewrite - ltn_sqr sb. by move:(subnK sa); rewrite - h => /square_plus2_square. by move/esym /square_plus2_square. move: (f_equal odd nv);rewrite eq2 /= -[12]/(6.*2)oddD oddM !odd_double. rewrite andbF /= => ob. have Hc: ((b==1) || (b==3) || (b== 9)). move: (Ha a b); move: (ltn_pmod n (ltn0Sn 11)). rewrite mulnC -nv (eqP eq1) -/b; move: ob Hb; clear. case:b => [| [|[|[|[| [| [|[|[|[| [| [| ]]]]]]] ]]]]] // _ Hb _. - by rewrite -[lucas 5]/(3 + 1 *8) addnC modnMDl => w; case Hb; rewrite w. - by rewrite -[lucas 7]/(5 + 3 *8) addnC modnMDl => w; case Hb; rewrite w. - by rewrite -[lucas 11]/(7 + 24 *8) addnC modnMDl => w; case Hb; rewrite w. set y := lucas (3*a + 4). have: lucas (12 * a + 9) = y * (y^2 +1). simpl. Abort. Lemma lucas_n_fib_mod5 n: n * lucas n == fib n %[mod 5]. Proof. pose Y n := n * lucas n - fib n. have Hx m: m != 0 -> fib m <= m * lucas m. move => h; apply:(@leq_trans (lucas m)); first by apply:fib_lt_lucas. by apply:leq_pmull; rewrite lt0n. have Ha: forall n, n != 0 -> n * lucas n = fib n + Y n. move => m /Hx h; rewrite /Y subnKC //. have Hb x y z: x + z = y -> x = y - z by move => <-; rewrite addnK. have Hc a b: a = 0 %[mod 5] -> b = 0 %[mod 5] -> a.*2+b = 0 %[mod 5]. by move => sa sb; rewrite - modnDm - addnn - (modnDm a a 5) sa sb mod0n. have Hd a b: a = 0 %[mod 5] -> b = 0 %[mod 5] -> a-b = 0 %[mod 5]. move => sa sb; case/orP:(leq_total a b); first by rewrite -subn_eq0 => /eqP->. by move/subnKC=> sc; move: sa; rewrite -{1}sc -modnDm sb mod0n add0n modn_mod. suff Hf : forall m, Y m.+4 = ((Y m.+3).*2 + Y m.+2) - ((Y m.+1).*2 + Y m). case nz:(n== 0); rewrite ? (eqP nz) // -(addn0 (fib n)) Ha ? nz // eqn_modDl. suff: (forall k, k <= n.+3 -> Y k = 0 %[mod 5]). by move => h; apply/eqP /h /ltnW /ltnW. clear nz;elim: n; first by case => [|[|[|[| ]]]]. move => n Hrec k. have ha: n < n.+3 by apply/ltnW/ltnW. have hb := (ltnW ha). rewrite (leq_eqVlt); case/orP; last by rewrite ltnS; apply: Hrec. move => /eqP ->; rewrite Hf; apply: Hd; apply: Hc;apply: Hrec => //. have He m: m!=0 -> (Y m.+1).*2 + Y m = (m.+1 * lucas m.+1).*2 + m * lucas m - ((fib m.+1).*2 + fib m). move => h; apply: Hb. rewrite addnACA -doubleD (addnC (Y m)) - Ha // (addnC (Y m.+1)) - Ha //. move => m; case mz: (m==0); first by rewrite (eqP mz). have mz' := (negbT mz). set x1 := (m.+1 * lucas m.+1).*2 + m * lucas m. set x2 := (fib m.+1).*2 + fib m. set x3 := (m.+3 * lucas m.+3).*2 + m.+2 * lucas m.+2. set x4 := (fib m.+3).*2 + fib m.+2. have la: x2 <= x1 by rewrite /x1 /x2; apply: leq_add; rewrite ? leq_double Hx. apply: (Hb); rewrite ! He //; apply: (Hb);rewrite addnAC (addnBA _ la). symmetry;apply:(Hb);rewrite -/x3 -/x4 - addnA [RHS]addnC (addnBA _ (Hx _ _)) //. apply:Hb;rewrite /x1 /x2 /x3 /x4; clear. rewrite (addnC _ ((fib m.+1).*2 + fib m)) addnAC - [in RHS] addnA; congr addn. by rewrite -fib3S - fib3S addnC -fibSS. rewrite {1} [m.+3] (addnC 3 m) {1} [m.+4] (addnC 4 m) !mulnDl doubleD doubleMr. rewrite addnAC {2} [m.+2] (addnC 2 m) mulnDl addnA - mulnDr (mulSn m) addnA. rewrite - (addnA _.*2) - mulnDr doubleD (doubleMr m) - (addnA _.*2) - mulnDr. rewrite (addnC (lucas m.+1).*2) -addnA - addnA; congr (m *_ + _). by rewrite -lucas3S addnA - lucas3S addnC -lucasSS. rewrite -(mulnA 2 2) ! mul2n - !doubleD; congr double. rewrite (lucasSS m.+2) doubleD addnA addnAC mulSn mul2n addnA; congr addn. by rewrite addnC - lucasSS lucas3S addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)