proposition: Lemma composite_fib n: natp n -> n <> \4c -> composite n -> composite (Fib n).
proof: Proof. move => nN n4 [a [aN a1 an dvd]]. case: (equal_or_not \2c a) => ea2. move: an n4. move:(cdivides_pr dvd); rewrite - ea2 -/(double _) -/(chalf _) => -> an n4. have kN:= (NS_half nN). apply: (composite_even_fib kN); split. case: (NleT_el NS2 kN) => // /clt2; case => eq; move:an; rewrite eq ?cprod0r ? (cprod1r CS2) => hh; first case: (clt0 hh). by case: (proj2 hh). by move => e1; case: n4; rewrite - e1 cprod_22. have a2: \2c <c a by split => //;rewrite - succ_one; apply /(cleSltP NS1). have anz:= (nesym (proj2 (clt_ltT clt_01 a1))). exists (Fib a); split => //. + by apply: NS_Fib. + apply: (Fib_gt1 aN a2). + apply: (Fib_smonotone aN nN anz (nesym (proj2 a1)) an). + exact(Fib_div dvd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)