proposition: Lemma fib_lucas1 j k: j <= k -> lucas j * fib k = (if (odd j) then subn else addn) (fib (k + j)) (fib (k - j)).
proof: Proof. case:j; first by rewrite /= addn0 subn0 mul2n addnn. move => j;rewrite leq_eqVlt; case/orP => ljk. rewrite (eqP ljk) mulnC - fib_double_lucas addnn subnn fib0. by case: odd => //; rewrite ?subn0 ?addn0. have hb: 0 < fib (k - j.+1) by rewrite fib_gt0 //subn_gt0. have ha:=(fib_sub (ltnW ljk)). rewrite mulnC lucas_fib // (addnC k) fib_add // mulnDr addnC. rewrite (mulnC _ (fib k)) (mulnC _ (fib k.+1)); move: ha; simpl. case:odd => /= ha; rewrite ha. by rewrite - addnA subnKC // ltnW // -subn_gt0 -ha. have hc : fib k * fib j.+2 < fib k.+1 * fib j.+1 by rewrite - subn_gt0 -ha. by rewrite - {1} (subnKC (ltnW hc)) addnA addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)