proposition: Lemma lucas_lucas1 p n: p <= n -> lucas n * lucas p = (if (odd p) then subn else addn) (lucas (n + p)) (lucas (n - p)).
proof: Proof. case: n; first by rewrite leqn0 => /eqP -> //. move => n; rewrite leq_eqVlt; case/orP; rewrite ?ltnS => ha. by rewrite - (eqP ha) addnn subnn mulnn lucas_square. rewrite mulnC (@lucas_fib n.+1) //= mulnDr subSn //. rewrite (fib_lucas1 (leqW (leqW ha))) (fib_lucas1 ha) lucas_fib //lucas_fib //. rewrite (subSn (leqW ha)) (subSn ha) addSn addSn /=. case:odd; last by rewrite addnACA. have hb:=leq_BD n p. have/subnK {2}<-: fib (n - p) <= fib (n + p) by apply: fib_monotone. have: fib (n - p).+2 <= fib (n + p).+2 by apply: fib_monotone; rewrite !ltnS. by move/subnK => {2} <-; rewrite addnACA addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)