proposition: Lemma fib_times_lucas_is_lucas n k m: lucas n == (fib m) * (lucas k) = [ || ((m==1) || (m==2)) && (n == k), ((k==1) && [|| (n==0) &&(m==3), (n==1) &&((m==1) || (m==2)) | (n==2)&&(m==4) ]) | [&& k ==0 , n == 3 & m ==3] ].
proof: Proof. have sc: (n == k) = false -> false = (k == 1) && (n == 1). by case k1: (k==1) => //;rewrite (eqP k1). case mz:(m==0). by rewrite (eqP mz) mul0n (gtn_eqF (lucas_gt0 n)) !andbF /=. case m1: (m==1). rewrite (eqP m1) /= mul1n lucas_injective_bis; case nk: (n == k) => //. by rewrite !andbF andbT /= !orbF; apply: sc. case m2: (m==2). rewrite (eqP m2) /= mul1n lucas_injective_bis; case nk: (n == k) => //. by rewrite !andbF andbT /= !orbF; apply: sc. case k1: (k==1). by rewrite (eqP k1) muln1 eq_sym fib_eq_lucas m1 m2 !andbF /= orbF. have lt1: 1 < m by move: mz m1; case m => [|[]]. have lt2: 2 < m by move: mz m1 m2; case m => [|[|[]]]. have ms1p: 0 < m.-1 by move: mz m1; case m => [|[]]. have ww := (ltn_predK lt1). case kz: (k==0). rewrite (eqP kz) lucas0 /=; case m3:(m==3). by rewrite (eqP m3) -[fib 3 * 2]/ (lucas 3) lucas_injective_bis andbT. rewrite andbF; apply /negbTE/eqP => eqa. move:(lucas_ge_2fib lt1); rewrite - muln2 -eqa => eqb. case: (ltnP m n) => lmn. have /lucas_smonotone :0 < m < n by rewrite (ltnW lt1) lmn. by rewrite ltnNge eqb. case nz: (n==0). move:(leq_mul2r 2 (fib 3) (fib m)); simpl; rewrite (fib_monotone lt2) - eqa. by rewrite (eqP nz) lucas0. case nt: (n==2). move: eqa; rewrite (eqP nt) muln2 => h; move:(f_equal odd h). by rewrite odd_double. have: fib m.+1 <= lucas n. by rewrite eqa muln2 -addnn -ww fibSS leq_add2l fib_monotone. move/leqifP:(lucas_lt_fib (negbT nz)); rewrite nt => ha hb. move:(leq_ltn_trans hb ha) => /fib_monotone_bis; rewrite !ltnS => hc. move: (eqn_leq m n); rewrite lmn hc /= => /eqP emn. move:eqa; rewrite - emn muln2 -addnn (lucas_fib (negbT mz)) - {1}ww. move/eqP; rewrite fibSS ww -addnA eqn_add2l eq_sym addnn - mul2n. by rewrite fib_times_c_is_fib3 mz -3!(eqSS m.-1) ww m1 m2 m3. simpl; apply/negP => /eqP h. have fp:= (fib_gt0 (ltnW lt1)). have lk3: 3 <= lucas k. by rewrite(lucas_monotoneE 2) /= orbF -leq_eqVlt ltn_neqAle eq_sym lt0n kz k1. have la: m < n. have b1 := (leq_mul (fib_monotone lt2) lk3). case nz: (n== 0); first by move: b1; rewrite - h (eqP nz). case n2: (n== 2); first by move: b1; rewrite - h (eqP n2). move/leqifP:(lucas_lt_fib (negbT nz)); rewrite n2 h. move: (ltnW lk3); rewrite - (leq_pmul2r fp) mul2n mulnC => sa sb. have lc : fib n.+2 <= (fib n.+1).*2. by rewrite fibSS -addnn leq_add2l fib_monotone //. move: (leq_trans (leq_ltn_trans sa sb) lc); rewrite ltn_double. move/fib_monotone_bis; rewrite ltnS leq_eqVlt; case/orP => // emn. move: lk3; rewrite - (leq_pmul2l fp) - h (eqP emn). move: nz n2; clear; case: n => //n _; rewrite lucas_fib // fibSS. rewrite mulnS -addnA leq_add2l /= muln2 addnn leq_double leqNgt. case: n => //; case => //n; rewrite fib_smonotone // !ltnS leqnn //. move: (lucas_add m.-1 (n-m)); rewrite -addnS ww (subnK (ltnW la)) => eq2. have: lucas (n - m).+1 * fib m < lucas n. rewrite eq2 ltn_paddr // muln_gt0 lucas_gt0 fib_gt0 //. rewrite h mulnC ltn_mul2l fp /= => lb. case: (ltnP (n - m).+1 k) => lc; last first. by move: lb; rewrite ltnNge lucas_monotone //lc lt0n kz. have:lucas (n - m) * fib m.-1 < lucas (n - m) * fib m. by rewrite ltn_mul2l lucas_gt0 /= fib_smonotone // - ltnS ww lt2 leqnn. rewrite -(ltn_add2l (lucas (n - m).+1 * fib m)) -eq2 h -mulnDl -lucasSS. by rewrite mulnC ltn_mul2r fp /= ltnNge lucas_monotone. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)