proposition: Lemma lin_fib_alt : forall n a b, lin_fib a b n.+2 = lin_fib a b n.+1 + lin_fib a b n.
proof: Proof. case=>//; elim => [//|n IHn] a b. by rewrite lin_fibSS (IHn b (b + a)) lin_fibE. Qed.
imports: mathcomp(all_ssreflect all_algebra)