Require Import Arith.
Fixpoint fib (n : nat) :=
match n with
0 => 1
| 1 => 1
| S (S p as x) => fib x + fib p
end.
Fixpoint fib_t (fibn fibsn p :nat) :=
match p with
0 => fibn
| S k => fib_t fibsn (fibsn + fibn) k
end.
Lemma mylemma : forall n p, fib_t (fib n) (fib (S n)) p = fib (n + p).
Proof.
intros n.
intros p.
revert n.
induction p.
simpl.
intros n.
replace (n + 0) with n by ring.
reflexivity.
intros n’.
replace (n’ + S p) with (S (n’ + p)) by ring.
replace (fib_t (fib n’) (fib (S n’)) (S p)) with (fib_t (fib (S n’)) (fib (S (S n’))) p).
rewrite IHp.
replace (S n’ + p) with (S (n’ + p)) by ring.
reflexivity.
simpl.
reflexivity.
Qed.
