proposition: Lemma lucasS n: lucas n.+1 = fib n.+1 + (fib n).*2.
proof: Proof. by rewrite (like_fibE lucas_like_fib) addnC mul1n mul2n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)