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