proposition: Lemma linear_fibo_equiv : forall n:nat, fib_tail n = fib n.
proof: Proof. intro n; induction n as [| | n IHn IHSn] using fib_ind. - reflexivity. - reflexivity. - unfold fib_tail in *; rewrite general_fib_2. rewrite IHn, IHSn; reflexivity. Qed.
imports: Arith fib_ind