proposition: Lemma lucas_powge2 n: 1 < lucas (2 ^ n.+1) ^ 2.
proof: Proof. by rewrite -{1}[1]/(1^2) ltn_sqr expn2S lucas_ge2d. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)