proposition: Lemma lucas_ge2d n: 1 < lucas (n.*2).
proof: Proof. by rewrite lucas_ge2 => //; case:n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)