proposition: Lemma lucas_pow2_mod4 n: lucas (2^(n.+1)) = 3 %[mod 4].
proof: Proof. case: n => // n; rewrite expn2S lucas_square' {1} expn2S odd_double. have aux:= (square_odd_mod4(lucas_pow2_odd n.+1)). by apply/eqP; rewrite -(eqn_modDr 2) subnK ?lucas_powge2 // aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)