proposition: Lemma lucas_lucas2 p n: p <= n -> 5 * fib n * fib p = (if (odd p) then addn else subn) (lucas (n + p)) (lucas (n - p)).
proof: Proof. elim: p {-2} p (leqnn p) => [p|p IHp p0]. by rewrite leqn0; move/eqP=>-> /=; rewrite /= addn0 subn0 subnn muln0. rewrite leq_eqVlt; case/orP=> [|Hn1]; last by apply: IHp; rewrite - ltnS. move /eqP => -> lnp. case wwa: (p == 0). move: lnp; rewrite (eqP wwa) => /subnK {1 2} <- /=. by rewrite muln1 addn1 addn1 lucasSS - addnA addnn lucas_fib3. case wwb: (p == 1). move: lnp; rewrite (eqP wwb) => /subnK {1 2} <- /=. set x := lucas (n - 2).+1. rewrite addn2 addn2 3!lucasSS muln1 lucas_fib2 (addnC x) - (addnA _ x x). by rewrite addnn - addnACA -mul2n -(mulSnr 2 x) - addnA addKn addnC. have Hg: (lucas (n - p.+1).+2).*2 = lucas (n - p.+1) + lucas (n - p.+1).+3. by rewrite addnC [in RHS] lucasSS - addnA -lucasSS addnn. case: (odd_dichot p) => pv; rewrite pv /= odd_double /=. case (posnP p./2) => ww; first by move: wwb; rewrite pv ww. move: (prednK ww) => eq1. have Ha: (p./2.-1).*2 < p by rewrite {2} pv ltnS leq_double leq_pred. have Hb: (p./2.-1).*2 < n by rewrite (ltn_trans Ha lnp). have Hc: (p./2).*2 <= p by apply: double_half_le. have Hd:= (leq_trans Hc (ltnW lnp)). have He: (p./2.-1).*2.+4 <= n by rewrite - doubleS eq1 - pv. rewrite fibSS mulnDr -{1} eq1 doubleS fibSS - doubleS eq1. rewrite mulnDr addnAC addnn IHp // IHp // /= !odd_double /=. rewrite - {1 2 5 6} eq1 doubleS ! addnS 2! [in RHS] lucasSS addnAC addnn. rewrite - {2 4}(subnK He) -2!addSnnS addnK - addSnnS addnK -doubleS eq1 -pv. set A := (lucas (n + (p./2.-1).*2).+2).*2. have lt1: lucas (n - p.+1) + lucas (n - p.+1).+3 <= A. rewrite - Hg /A leq_double; apply: lucas_monotone => /=. by apply: (@leq_trans n.+2); rewrite !ltnS ? leq_subr // ?leq_addr. move/ (leq_sub2r (lucas (n - p.+1))): (lt1); rewrite addKn => lt2. rewrite doubleB Hg subnDA addnC - addnA subnKC // [in RHS] addnC - addnBA //. apply: leq_trans lt1; apply leq_addr. case (posnP p./2) => ww; first by move: wwa; rewrite pv ww. move: (prednK ww) => eq1; rewrite - eq1 doubleS. have Ha: (p./2.-1).*2 < p by rewrite {2} pv ltn_double eq1. have Hc := leq_trans Ha (ltnW lnp). have Hb:= ltnW Ha; have Hd:= ltnW Hc. have Ht: (n - (p./2.-1).*2) = (n-p.+1).+3. by rewrite -3! subSS - doubleS eq1 - pv -{1} (subnK lnp) - 3!addSn addnK. have He: lucas (n - p.+1).+3 <= lucas (n + (p./2.-1).*2). apply: lucas_monotone; rewrite /= - Ht; apply: leq_BD. have Hf: (p./2.-1).*2.+3 <= n by rewrite -doubleS eq1 - pv. rewrite fibSS fibSS addnC addnA addnn mulnDr - doubleMr IHp // IHp //=. rewrite odd_double /= doubleD !addnS lucasSS lucasSS [ X in _ = X + _] addnAC. have ->: (n - (p./2.-1).*2.+3) = n - p.+1 by rewrite - doubleS eq1 - pv. have ->: (n - (p./2.-1).*2.+1) = (n-p.+1).+2. by rewrite -2! subSS - doubleS eq1 - pv -{1} (subnK lnp) - 2!addSn addnK. rewrite addnn -!addnA Ht (addnBA _ He) Hg; congr addn. by rewrite addnC addnA addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)