proposition: Lemma composite_even_fib n: natp n -> \2c <c n -> composite (Fib (cdouble n)).
proof: Proof. move => nN n2; case: (equal_or_not n \0c) => nz. by case:(proj2 (clt_ltT clt_02 n2)). move:(nN) n2;move: (cpred_pr nN nz) => [sa ->] sN n2. have ha:= NS_Fib sN. have hb:= NS_Fib sa. have hc:= (NS_sum (NS_double hb) ha). have hd := (Fib_gt1 sN n2). rewrite (Fib_even sa); apply:(composite_prod ha hc hd). apply: (clt_leT hd); apply:(Nsum_Mle0 _ ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)