proposition: Lemma FR_lucas1 n: FR (lucas n.+3) = n./2.*2.+1.
proof: Proof. have h: 1 < n +2 by rewrite addn2 !ltnS. by move: (FR_fib_sum1 0 h); rewrite addn2 lucas_fib // muln2 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)