proposition: Lemma lucas_times_lucas_is_lucas m n k: k <= m -> lucas n == (lucas m) * (lucas k) = [ || [&& k ==0, m == 0 & n == 3], [&& k ==0, m == 1 & n == 0] | [&& k ==1 & m == n] ].
proof: Proof. move => km. case kz: (k==0). rewrite mulnC (eqP kz) -[lucas 0]/(fib 3) fib_times_lucas_is_lucas. by rewrite /= ! andbF !orbF eqxx !andbT orbC. case k1: (k==1). by rewrite mulnC (eqP k1) lucas1 mul1n /= lucas_injective_bis. simpl; apply/negP => /eqP; rewrite lucas_lucas1 //. have ha: 1 < k by rewrite ltn_neqAle lt0n kz eq_sym k1. have hb:=(leq_add (leq_trans ha km) ha). have x0:= (gtn_eqF(ltnW (ltnW(ltnW hb)))). have x1 :=(gtn_eqF (ltnW(ltnW hb))). case ok: (odd k); last first. move/eqP; rewrite addnC lucas_plus_lucas ? leq_BD // x0 x1 !andbF /=. rewrite -{1} (subnKC km) addnAC addnn - add1n eqn_add2r. by move/andP => [/eqP ea _]; move:(f_equal odd ea); rewrite odd_double. case: (ltnP (lucas (m + k)) (lucas (m - k))) => hh. by rewrite (eqP (ltnW hh))=> h; move: (lucas_gt0 n); rewrite h. move => hc. have: lucas (m + k) == lucas (m - k) + lucas n. by rewrite - {1} (subnK hh) - hc addnC. case /orP: (leq_total (m - k) n) => la. rewrite lucas_plus_lucas // (gtn_eqF hb) x0 /= => /andP[_]. by rewrite - {1} (subnK km) -addnA -addn2 eqn_add2l addnn (eqn_double k 1) k1. rewrite (addnC (lucas _)) lucas_plus_lucas // (gtn_eqF hb) x0 /= => /andP[]. move/eqP => <- /eqP ea; move:(f_equal odd ea). by rewrite -{1} (subnK km) -addnA addnn oddD /= odd_double addbF; case:odd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)