proposition: Lemma lucas_lucas4 n p: (fib (n + p)).*2 = lucas n * fib p + lucas p * fib n.
proof: Proof. wlog le1: n p / p <= n. move => H; case/orP: (leq_total p n); first by apply:H. by move => ha; rewrite addnC H // addnC. have ha: fib (n - p) <= fib (n + p) by apply: fib_monotone; apply:leq_BD. rewrite (fib_lucas1 le1) (fib_lucas2 le1) -addnn (addnC p). by case: odd; [ rewrite - addnA subnKC | rewrite addnCA subnK]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)