proposition: Lemma fib_times_c_is_fib3 n k : fib n == 2 * (fib k) = ((k==0) && (n==0)) || ((n==3) && ((k==1) || (k==2))).
proof: Proof. rewrite (lucas_times_fib_is_fib k n 0) andbF !orbF /= (eq_sym 0 k). by case kz: (k==0); rewrite ? orbF // (eqP kz) !andbF orbb orbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)