proposition: Lemma lucas_square' n: lucas (n.*2) = (if (odd n) then addn else subn) ( (lucas n)^2) 2.
proof: Proof. by rewrite lucas_square; case: odd; rewrite ? addnK // subnK // lucas_ge2d. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)