proposition: Lemma lucas_times_lucas_is_fib m n k: k <= m -> (fib n == (lucas m) * (lucas k)) = [|| [&& k==0, m == 1 & n == 3], [&& k==0, m == 3 & n == 6], (k==1) && [|| (m == 1) && (n == 1), (m == 1) && (n == 2) | (m == 2) && (n == 4)] | [&& k ==2, m==4 & n==8] ].
proof: Proof. move => h. case kz: (k == 0). by rewrite (eqP kz) -[lucas 0]/(fib 3) lucas_times_fib_is_fib !andbF !orbF. case kn1: (k == 1). move:h;rewrite (eqP kn1) muln1 fib_eq_lucas /= lt0n; case: eqP => // _ _. by case m1: (m==1); rewrite orbF // (eqP m1) andFb !orbF. have sk := (subnK h). simpl;apply/eqP/idP; last by move/and3P => [/eqP -> /eqP -> /eqP ->]. have mkz: m + k != 0 by rewrite addn_eq0 kz andbF. have la: 2 <= k by move: kz kn1; case:(k) => //; case. have mk2:=(leq_add (leq_trans (ltnW la) h) (ltnW la)). move:(subnK mk2); rewrite addn2 => hb. rewrite (lucas_lucas1 h); case ok: (odd k); last first. rewrite (lucas_fib mkz) => ea. have: fib (m + k).+1 < fib n. by rewrite ea -addnA -[X in X < _] addn0 ltn_add2l addn_gt0 lucas_gt0 orbT. move/fib_monotone_bis => /fib_monotone. rewrite ea -addnA fibSS leq_add2l -hb fibSS leq_add2l. move:h; rewrite leq_eqVlt; case/orP => hc. move: ea;rewrite - (eqP hc) subnn lucas0 - ltnS -[3]/(fib 4) => fn h. move: (fib_monotone_bis h) fn kz ok; case k => //; case => //; case => //. rewrite -[RHS ]/9 => _ eb _ _; case: (ltngtP 7 n) => sa. + by move:(@fib_smonotone 7 n); rewrite eb sa /=; apply. + by rewrite ltnS in sa;move:(fib_monotone sa); rewrite eb. + by move: eb; rewrite - sa. by move => n1; rewrite !addnS !addSn /= subn2 !ltnS ltn0. move: (hc); rewrite - subn_gt0 => /gtn_eqF /negbT/lucas_lt_fib /leqifP. move:ea; rewrite - [in m+k] sk - !addnA addnn. case ha: (m-k==2). rewrite -[in m==4] sk (eqP ha) addKn. move: kz ok; clear; case: k => [| [| [ | k ]]]//. move => _ _; rewrite -[RHS]/(fib 8) => /eqP. by rewrite fib_eq !andbF !orbF. move => _ _ _ _ h. have: 2 < (k.+2).*2 by rewrite !doubleS !ltnS. by move /fib_smonotone_bis; rewrite ltnNge h. move => ea lc lb; move:(leq_ltn_trans lb lc) => /fib_monotone_bis. move: kz ok; clear; case: k => [| [| k]] // _ _. by rewrite !doubleS -(addn2 k.*2.+2) addnA addnK - 2!addSnnS ltnNge leq_addr. move:h;rewrite leq_eqVlt; case/orP => lkm. rewrite - (eqP lkm) subnn lucas0; move: ok kn1; clear; case:k => //k. rewrite addnS addSn addnn lucas_fib //=; case:k => // k ok _. have e2: 2 < fib (k.+1).*2.+1. apply: (fib_monotone(m:=4)); rewrite doubleS !ltnS double_gt0. by move:ok;case:(k). rewrite -(addnBA _ (ltnW e2)) => eq1. have: fib (k.+1).*2.+3 < fib n. by rewrite eq1 -[X in X < _] addn0 ltn_add2l subn_gt0. move/fib_monotone_bis => /fib_monotone; rewrite fibSS eq1 leq_add2l fibSS. by rewrite -{1} (subnK (ltnW e2)) -addnA leqNgt add2n addnS ltnS leq_addr. move => ea. have mkgt4:=(leq_add (leq_ltn_trans la lkm) la). have eb: fib n + lucas (m - k) = lucas (m + k). rewrite ea subnK // lucas_monotone // subn_gt0 lkm /=; apply: leq_BD. move /leqifP: (lucas_lt_fib mkz). rewrite eq_sym (ltn_eqF (ltnW(ltnW mkgt4))) - eb => bnd1. move:(leq_ltn_trans (leq_addr (lucas (m - k)) (fib n)) bnd1). move => /fib_monotone_bis; rewrite ltnS => /fib_monotone. rewrite -(leq_add2r (lucas (m - k))) eb (lucas_fib mkz) leq_add2l => bnd2. move:lkm; rewrite leq_eqVlt; case/orP => lkm1. move: bnd2; rewrite - (eqP lkm1) subSnn addSn addnn /=. have: 1 < 3 < k.*2 by move: kz kn1; clear; case:k => [|[|]]//. by move /fib_smonotone => hu hv; move:(leq_trans (ltnW hu) hv). move:lkm1; rewrite leq_eqVlt; case/orP => lkm2. move: bnd2; rewrite - (eqP lkm2) - (add2n k) addnK -addnA addnn add2n. rewrite -[lucas 2]/(fib 4) leqNgt fib_smonotone //= ltnS (leq_double 2 k). by move: kz kn1; clear; case:k => [|[|]]//. move:(lkm2);rewrite - addn2 addSn -ltn_subRL => wa. move/leqifP: (lucas_lt_fib (negbT (gtn_eqF (ltnW(ltnW wa))))). rewrite (gtn_eqF wa) => wb. move:(fib_monotone_bis (leq_ltn_trans bnd2 wb)). rewrite ltnNge - {2} sk -addnA addnn - {3} (ltn_predK la) doubleS !addnS. rewrite !ltnS -{1} (addn0 (m-k)) ltn_add2l double_gt0. by move:kz kn1;clear; case: k => [| [| ]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)