proposition: Lemma lucas_mod3 n: 3 %| (lucas n) = (n== 2 %[mod 4]).
proof: Proof. case:n => [| [| n ]] //. rewrite -{3} (add0n 2) - {2} (addn2 n) eqn_modDr - (add1n n) lucas_add /dvdn. rewrite mul1n mulnC modnMDl; exact:fib_mod3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)