proposition: Lemma fib_prime : forall p, p != 4 -> prime (fib p) -> prime p.
proof: Proof. move=> p Dp4 Pp. apply/primeP; split; first by case: (p) Pp => [|[]]. move=> d; case/dvdnP=> k Hp. have F: forall u, (fib u == 1) = ((u == 1) || (u == 2)). case=> [|[|[|n]]] //; case: eqP=> // Hm; have: 1 < 2 < n.+3 by []. by move/fib_smonotone; rewrite Hm. 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 -[X in X == _ -> _]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(all_ssreflect all_algebra)