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