proposition: Lemma fib_eq_lucas m n: (fib m == lucas n) = [|| (n==0) &&(m==3), (n==1) &&((m==1) || (m==2)) | (n==2)&&(m==4) ].
proof: Proof. case nz: (n==0). by rewrite (eqP nz) lucas0 (fib_eq m 3) !andbF. have ha:= (leq_ltn_trans (leq_pred n) (ltnSn n)). rewrite lucas_fib ? nz // addnC (fib_plus_fib _ (ltnW ha)) (ltn_eqF ha) !eqSS. have hc:=(prednK (neq0_lt0n nz)). case no: (n==1); first by rewrite (eqP no) /= fib_eq andbF !orbF andbT orbC. case nt: (n==2); first by rewrite (eqP nt) /= orbF. by rewrite - eqSS hc no andbF /= - {1} hc (gtn_eqF (ltnSn n.-1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)