proposition: Lemma like_fib_bis F: like_fib F -> F 0 <= 2 * F 1 -> forall n, 2 * F n = (F 0) * (lucas n) + (2* (F 1) - F 0)* (fib n).
proof: Proof. have Ha:= lucas_like_fib. move => h la. apply:like_fib_eq. + by apply: like_fib_mul. + by apply: like_fib_add; apply: like_fib_mul. + by rewrite mulnC muln0 addn0. + by rewrite !muln1 subnKC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)