proposition: Lemma fib_times_fib_is_lucas m n k: k <= m -> lucas n == (fib m) * (fib k) = [|| (m==3) && [|| (k==1) && (n==0), (k==2) && (n==0) | (k==3) && (n==3)], (k==1) && [|| (n==1)&&(m==1), (n==1) &&(m==2) | (n==2) && (m==4) ] | (k==2) && [|| (n==1) &&(m==2) | (n==2) && (m==4) ] ].
proof: Proof. set H := lucas_injective_bis. case m3:(m==3). rewrite (eqP m3) mulnC (fib_times_lucas_is_lucas n 0 k) /= !andbF !orbF. by rewrite orbA - andb_orl (andbC (k == 3)). case k1: (k == 1). rewrite /= (eqP k1) muln1 eq_sym (fib_eq_lucas) /=. case n0: (n==0); first by rewrite (eqP n0) /= m3. by case n1: (n==1); rewrite orbF // (eqP n1) /= !orbF. case k2: (k == 2). rewrite /= (eqP k2) muln1 eq_sym (fib_eq_lucas) m3 /= => /gtn_eqF ->. by rewrite andbF. move => le1 /=;apply/negP => h. case:(ltnP k 4) => k4. move: k4;rewrite leq_eqVlt eqSS; case /orP => k4. move: le1 h; rewrite (eqP k4) (fib_times_lucas_is_lucas n 0 m) => m2. by rewrite m3 (gtn_eqF m2) (gtn_eqF (ltnW m2)) /= andbF. move: k4; rewrite !ltnS leq_eqVlt k2 ltnS leq_eqVlt k1 ltnS leqn0 /= =>/eqP. by move => kz; move: (gtn_eqF (lucas_gt0 n)); rewrite (eqP h) kz muln0. move: (f_equal (muln 5) (eqP h));rewrite mulnA lucas_lucas2 // => h1. have la: m < m + k by rewrite -{1} (addn0 m) ltn_add2l (ltnW (ltnW(ltnW k4))). have bnd1:= (leq_add (leq_trans (ltnW k4) le1) k4). have bnd2 :=(subnK (ltnW(ltnW bnd1))). set q := (m + k - 5) in bnd2. move:(lucas5S q); rewrite bnd2 => ea. have eb: lucas (m - k) <= lucas q. case emk: (k==m). rewrite -(eqP emk) subnn; apply: ltnW; apply:(@lucas_monotone 2). by rewrite /= -(leq_add2r 5) bnd2 bnd1. have mp:=(ltn_predK (leq_trans k4 le1)). have mp1: m - k <= m.-1 by rewrite -(leq_add2r k) (subnK le1) -ltnS -addSn mp. apply: lucas_monotone;rewrite subn_gt0 ltn_neqAle emk le1 (leq_trans mp1) //. by rewrite -(leq_add2r 5) bnd2 -addSnnS mp leq_add2l. have: lucas (m - k) < 2 * lucas q. by apply: (leq_ltn_trans eb); rewrite -[X in X< _] mul1n ltn_mul2r lucas_gt0. rewrite - (ltn_add2l (lucas (m + k))) => sa. have sb: 5 * lucas n <= (lucas (m + k)) + (lucas (m - k)). rewrite h1; case: odd => //; apply: leq_BD. move: (leq_ltn_trans sb sa); rewrite ea - addnA -mulnDl - mulnDr - lucasSS. rewrite ltn_mul2l /= => e1. case: (ltnP q.+1 n) => e3. have: 0 < q.+2 <= n by []. by move/lucas_monotone; rewrite leqNgt e1. have ec: (lucas (m + k)) - (lucas (m - k)) <= 5 * lucas n. rewrite h1; case: odd => //; apply: leq_BD. have: 0 < (2 * lucas q + (lucas q - lucas (m - k))). move:(lucas_gt0 q); rewrite - double_gt0 - mul2n => pa. apply: (leq_trans pa); apply: leq_addr. move:(addnBA (5 * lucas q.+1 + 2 * lucas q) eb). rewrite - 2!addnA -mulSnr - ea -(ltn_add2l (5* lucas q.+1)) addn0. move => -> ed; move: (leq_trans ed ec); rewrite ltn_mul2l /= ltnNge => /negP. case; case: (posnP n) => np; last by apply: lucas_monotone; rewrite np e3. have: 0 < 3 <= q.+1 by rewrite /= -ltnS ltnS ltnS -(leq_add2r 5) bnd2. by move/lucas_monotone; apply: leq_trans; rewrite np. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)