proposition: Lemma Fib_is_even_mod3 n: natp n -> (evenp (Fib n) <-> \3c %|c n).
proof: Proof. have H: forall m, natp m -> evenp (Fib (\3c *c m)). move => m mN. by move:(Fib_div (cdivides_pr1 mN NS3)); rewrite Fib3; move => [sa _ sb]. have aux: forall k, natp k -> csucc (csucc k) = k +c \2c. move => k kN. by rewrite - csum_11 csumA (Nsucc_rw (NS_succ kN)) (Nsucc_rw). suff H1:forall n, natp n -> oddp (Fib (csucc (\3c *c n))) /\ oddp (Fib (csucc (csucc (\3c *c n)))). move => nN;split; last first. by move/cdivides_pr => ->; apply: H; apply: NS_quo. move: NS3 => n3 ef. move:(cdivision nN n3 card3_nz) => [sa sb [sc sd]]; split => //. have ha := (NS_prod n3 sa). move: (H1 _ sa); rewrite (aux _ ha) (Nsucc_rw ha); move => [[_ eqa] [_ eqb]]. by case: (div3_vals nN) => //eq1; move: ef; rewrite sc eq1. apply: {n} Nat_induction. rewrite cprod0r succ_zero succ_one Fib2 Fib1;split; apply odd_one. move => n nN [_ Hrec]; move:(NS_succ nN) => sN. have hc: natp (\3c *c n +c \2c) by apply: (NS_sum (NS_prod NS3 nN) NS2). have ha:= NS_prod NS3 sN. suff hb: oddp (Fib (csucc (\3c *c csucc n))). rewrite (Fib_rec ha); split => //; exact:(csum_of_even_odd (H _ sN) hb). rewrite (cprod_nS _ nN) {2} /card_three (csum_nS _ NS2) (Fib_rec hc). rewrite csumC - (csum_nS _ NS2) -/card_three - (cprod_nS _ nN). by rewrite - {1} (aux _ (NS_prod NS3 nN)); apply:(csum_of_even_odd (H _ sN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)