proposition: Lemma FR_lucas4 k j: j.*2.+2 <= k -> 1 <= j -> FR (lucas (j.*2) * (fib k)) = j.*2 + (j.*2.+1)*(k./2-j-1).
proof: Proof. move => h h1. rewrite (fib_lucas1 (ltnW(ltnW h))) odd_double. have lt1: 1 < k - j.*2 by rewrite -(subnK h) -(add2n j.*2) addnA addnK addn2. have lt2: j.*2 <= k by apply: leq_trans h; rewrite - addn2 leq_addr. have eb: (j * 4).-2.+2 = j.*2.*2. by rewrite - (prednK h1) mulSnr addn4 /= -addn4 -mulSnr -!muln2 -mulnA. have ea:(k + j.*2) = (j*4).-2 + (k - j.*2).+2. rewrite - addSnnS - addSnnS eb - (addnn j.*2) - addnA subnKC // addnC//. rewrite ea (FR_fib_sum1 _ lt1) eb /= doubleK uphalf_double mulnC. by rewrite -{2}(subnK lt2) halfD odd_double doubleK andbF add0n addnK subn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)