proposition: Lemma fib_prime p: p != 4 -> prime (fib p) -> prime p.
proof: Proof. move=> Dp4 Pp. apply/primeP; split; first by case: (p) Pp => [|[]]. move=> d; case/dvdnP=> k Hp. case/primeP: (Pp); rewrite Hp => _ Hf. case/orP: (Hf _ (dvdn_fib (dvdn_mulr d (dvdnn k)))). rewrite fib_eq1; case/orP; first by move/eqP->; rewrite mul1n eqxx orbT. move/eqP=> Hk. case/orP: (Hf _ (dvdn_fib (dvdn_mull k (dvdnn d)))). rewrite fib_eq1; case/orP; first by move->. by move/eqP=>Hd; case/negP: Dp4; rewrite Hp Hd Hk. rewrite fib_eq; case/or3P; first by move/eqP<-; rewrite eqxx orbT. by case/andP=>->. by rewrite Hk; case: (d)=> [|[|[|]]]. rewrite fib_eq; case/or3P; last by case/andP;move/eqP->; case: (d)=> [|[|]]. rewrite -{1}[k]muln1; rewrite eqn_mul2l; case/orP; move/eqP=> HH. by move: Pp; rewrite Hp HH. by rewrite -HH eqxx. by case/andP; move/eqP->; rewrite mul1n eqxx orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)