proposition: Lemma fib_lucas2 j k: k <= j -> lucas j * fib k = (if (odd k) then addn else subn) (fib (k + j)) (fib (j - k)).
proof: Proof. case:j; first by rewrite leqn0 => /eqP ->. 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 (j.+1 - k) by rewrite fib_gt0 //subn_gt0. rewrite addnC fib_add // lucas_fib // mulnDl // addnC. move: (fib_sub (ltnW ljk))=> ha; rewrite ha /=;move: ha; case:odd => ha. by rewrite -addnA subnKC // ltnW // -subn_gt0 -ha. have: (fib j.+2 * fib k < fib j.+1 * fib k.+1) by rewrite - subn_gt0 -ha. by move => /ltnW/subnKC {1} <-; rewrite addnA addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)