proposition: Lemma fib_times_c_is_fib5 n k m: 2 < k -> 2 < m -> fib n <> fib m * fib k.
proof: Proof. wlog: k m / k <= m. case /orP:(leq_total k m) => // ha hb. by apply: hb. by move => hc h; rewrite mulnC; apply: hb. move => sb sa _ h. have m3 := (leq_trans sa sb). have ms:= (ltn_predK m3). have ha: m.+1 != 0 by []. have hb: m != 0 by rewrite -ms. have hc: 0 < m.-1 by rewrite - ltnS ms (ltnW m3). have fmp: (0 < fib m) by rewrite fib_gt0 // lt0n. have lmn: m < n. apply/fib_monotone_bis; rewrite h -{1} (muln1 (fib m)) ltn_mul2l. rewrite fmp; apply:(fib_monotone sa). move:(fib_add (n-m) hb); rewrite (subnKC (ltnW lmn)) => eq1. have : fib m * fib (n - m).+1 < fib n. by rewrite eq1 ltn_paddl // muln_gt0 !fib_gt0 ?subn_gt0. rewrite h ltn_mul2l fmp /= => /fib_monotone_bis => la. have: fib m.-1 * fib (n - m) < fib m * fib (n - m). by rewrite ltn_mul2r fib_gt0 ?subn_gt0 //= fib_smonotone // -ltnS ms m3 leqnn. rewrite -(leq_add2r (fib m * fib (n - m).+1)) addSn - eq1 -mulnDr addnC. rewrite - fibSS h ltn_mul2l fmp // => /fib_monotone_bis; rewrite ltnS. by rewrite leqNgt la. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)