proposition: Lemma like_fib_lucas F: like_fib F -> F 0 <= 2 * F 1 -> F 1 <= 3 * (F 0) -> forall n, 5 * F n = (3* (F 0) - F 1) * (lucas n) + (2* (F 1) - F 0)* (lucas n.+1).
proof: Proof. have Ha:= lucas_like_fib. move => h la lb. move: (subnK la) (subnK lb); set a := _ - _; set b := _ - _ => ea eb. apply:like_fib_eq. + exact: like_fib_mul. + by apply: like_fib_add; apply: like_fib_mul. + apply/eqP; rewrite lucas0 lucas1 muln1 -(eqn_add2l (2 * F 1)) (mulnC b 2). by rewrite addnA - mulnDr (addnC _ b) eb - ea - addnA addnC -mulSn mulnA. + apply/eqP;rewrite lucas1 muln1 -[lucas 2]/3 -(eqn_add2r (3 * F 0)). by rewrite (mulnC a) - addnA - mulnDr ea mulnA (mulSn 5) addnA eb addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)