proposition: Lemma fib_times_c_is_fib1 n k c: k !=1 -> k != 2 -> fib n = c * (fib k) -> k %| n.
proof: Proof. move => k1 k2 h. move:(gcd_fib n k); rewrite h gcdnC gcdnMl => /esym /eqP. by rewrite fib_eq (negbTE k1) (negbTE k2) !andbF !orbF => /eqP /gcdn_idPr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)