proposition: Lemma fib_times_c_is_fib2 n k c: 2 <= c -> 2 < k -> fib n = c * (fib k) -> (lucas k) <= c.
proof: Proof. move => ha hb hc. have fkz:(fib k == 0) = false. by rewrite fib_eq0 eqn0Ngt (ltnW (ltnW hb)). case k1:(k==1); first by move:hb; rewrite (eqP k1). case k2:(k==2); first by move:hb; rewrite (eqP k2). move:(fib_times_c_is_fib1 (negbT k1) (negbT k2) hc) => /dvdnP [a nv]. move: hc; rewrite nv => /eqP. case: (ltngtP a 1). + rewrite ltnS leqn0 => /eqP ->. by rewrite eq_sym muln_eq0 fkz eqn0Ngt (ltnW ha). + move => sa sb. have: 2 *k <= a * k by rewrite leq_mul2r sa orbT. move/fib_monotone; rewrite mul2n fib_double_lucas (eqP sb) mulnC. by rewrite leq_mul2r fkz. + by move ->; rewrite mul1n - {1}(mul1n (fib k)) eqn_mul2r fkz (ltn_eqF ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)