proposition: Lemma lucas_times_fib_is_fib m n k: (fib n == lucas k * fib m) = [|| [&& k==0, n==3 & (m==1) || (m==2) ], (k==1) && [|| n == m, (n == 1) && (m == 2) | (n == 2) && (m == 1)] , ( ((m==0) && (n == 0)) || [&& ((m==1) || (m==2)), (k==2) &(n==4) ]) | (k==m) && (n == m.*2)].
proof: Proof. case mz: (m==0). by rewrite (eqP mz) muln0 fib_eq0; case nz:(n== 0); rewrite ?orbT //= !andbF. case m12: ((m == 1) || (m == 2)). have ->: fib m = 1 by case/orP:m12 => /eqP ->. rewrite muln1 fib_eq_lucas andbT /=; case:((k == 0) && (n == 3)) => //=. case n1: (n ==1). rewrite (eqP n1) andbT andbF /= !orbF (eq_sym 1 m) m12 andbT. by case:(orP m12) => /eqP ->; rewrite andbF orbF. case n4: (n ==4). rewrite /= (eqP n4) andbT !andbF /= orbF. by case:(orP m12) => /eqP ->; rewrite !andbF ?orbF // andbT/= orbb. rewrite andbF /= orbF;case:(orP m12)=> /eqP ->. by rewrite n1 /= andbT orbb. by rewrite n4 !andbF !orbF. have [ha hb]: (m==1) = false /\ (m==2) = false by move: m12; case: eqP. rewrite !andbF /=; case kz: (k==0). rewrite (eqP kz) lucas0 mul2n -addnn fib_plus_fib //= (eq_sym 0 m). by rewrite mz /= m12 /= andbF ha (ltn_eqF (ltnSn m)). case k1: (k==1). by rewrite (eqP k1) mul1n fib_eq (eq_sym 1) ha hb /= !andbF !orbF. have mk5: (5 <= m + k). have k2: 2 <= k by rewrite ltn_neqAle lt0n eq_sym k1 kz. have m3: 3 <= m by rewrite ltn_neqAle ltn_neqAle lt0n eq_sym hb eq_sym mz ha. exact: (leq_add m3 k2). move: (gtn_eqF mk5) (gtn_eqF (ltnW mk5)) (ltnW(ltnW mk5))=> mk4 mk3 mk5'. move: (gtn_eqF mk5') (gtn_eqF (ltnW mk5')) => mk2 mk1. have Hw p: p.*2 ==1 = false by case:p. have LTD m' k': (k' == 0) = false -> m' - k' < m' + k'. move => k'z; apply:(leq_ltn_trans (leq_subr k' m')). by rewrite ltn_paddr // lt0n k'z. case: (ltngtP m k) => hc; last first. + rewrite hc mulnC - fib_double_lucas fib_eq -[2]/(1.*2) eqn_double k1. by rewrite Hw !andbF !orbF. + rewrite (fib_lucas1 (ltnW hc)) /=; apply/negP => /eqP. have hd:= (LTD m k kz). case: odd; last first. move/eqP;rewrite addnC (fib_plus_fib _ (ltnW hd)) subn_eq0 leqNgt mk3 mk2. rewrite hc (ltn_eqF hd) /= - [in m +k](subnK (ltnW hc)) - addnA addnn. by rewrite andbF /= - addn1 eqn_add2l Hw. move: (subnK (ltnW hc)) => he ea. move/eqP :(esym (subnK (fib_monotone (ltnW hd)))); rewrite - ea. case /orP: (leq_total n (m - k)) => cnmk; [ | rewrite (addnC (fib n)) ]; rewrite (fib_plus_fib _ cnmk) mk4 mk3 !andbF /=. case/orP; first by rewrite fib_eq (gtn_eqF hd) /= mk1 mk2 /= andbF. rewrite - {2} he - addnA addnn => /andP[/eqP ->] /eqP h. by move:(f_equal odd h); rewrite oddD odd_double addbF /=;case:odd. rewrite subn_eq0 leqNgt hc /= - {2} he => /andP[_]. by rewrite -addnA -addn2 eqn_add2l addnn (eqn_double _ 1) k1. + rewrite (fib_lucas2 (ltnW hc)) ; apply/negP => /eqP. have he:= (subnKC (ltnW hc)). move: (LTD k m mz); rewrite addnC => hd. case: odd. move/eqP; rewrite addnC (fib_plus_fib _ (ltnW hd)) subn_eq0 mk1 mk2 mk3. by rewrite !andbF leqNgt hc //= -{1} he addnA addnn -add1n eqn_add2r Hw. move => ea. have: fib (m + k) == fib n + fib (k - m). by rewrite ea; rewrite subnK // (fib_monotone (ltnW hd)). case /orP: (leq_total n (k - m)) => cnmk;[ | rewrite (addnC (fib n)) ]; rewrite (fib_plus_fib _ cnmk) mk4 mk3 !andbF /=. case/orP; first by rewrite fib_eq (gtn_eqF hd) /= mk1 mk2 /= andbF. rewrite - {2} he addnA addnn => /andP[/eqP ->] /eqP h. by move:(f_equal odd h); rewrite oddD odd_double /=;case:odd. rewrite subn_eq0 leqNgt hc /= - {2} he => /andP[_]. by rewrite addnA -add2n eqn_add2r addnn (eqn_double _ 1) ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)