proposition: Lemma fib_double_lucas : forall n, fib (n.*2) = fib n * lucas n.
proof: Proof. case=> [|n]; rewrite // -addnn fib_add // lucas_fib // mulnDr addnC. by apply/eqP; rewrite eqn_add2l mulnC. Qed.
imports: mathcomp(all_ssreflect all_algebra)