proposition: Lemma fib_is_linear : fib =1 lin_fib 0 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 fibSS lin_fib_alt. by rewrite (IHn _ ltn0n) (IHn _ (ltnW ltn0n)). Qed.
imports: mathcomp(all_ssreflect all_algebra)