proposition: Lemma lucas_is_linear : lucas =1 lin_fib 2 1.
proof: Proof. move=>n; elim: n {-2}n (leqnn n)=> [n|n IHn]. by rewrite leqn0; move/eqP=>->. case=>//; case=>// n0; rewrite ltnS=> ltn0n; rewrite lucasSS lin_fib_alt. by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)). Qed.
imports: mathcomp(all_ssreflect all_algebra)