proposition: Theorem FR_fib7 k: FR (fib k.+3).-2 = (k.+2)./2.
proof: Proof. have H: forall u, FR (fib u.*2.+3).-2 = u.+1. elim; first by rewrite FR_0. by move => n Hr; rewrite - doubleS FR_fib6 // ! doubleS FR_fib5 Hr. rewrite -(odd_double_half k); case: (odd k). by rewrite FR_fib5 H /= uphalf_double. by rewrite H /= doubleK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)