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