proposition: Lemma fib_mod3 n: 3 %| (fib n) = (4 %| n).
proof: Proof. pose p n := (3 %| fib n) = (4 %| n). suff: [/\ p n, p n.+1, p n.+2 & p n.+3] by case. elim: n => // n [ha hb hc hd]; split => //. move: ha;rewrite /p fib4S - (addn4 n) /dvdn modnDr mulnC modnMDl. move => <-; rewrite - addnn - modnDm. by move: (mod3_small (fib n)); case: (fib n %% 3) => [|[|[|]]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)