Require Export Arith.
Require Export ArithRing.
Require Export ZArith.

Fixpoint fib (n:nat) : nat :=
  match n with
    0 => 1
  | 1 => 1
  | S ((S p) as q) => fib p + fib q
  end.

Functional Scheme fib_ind := Induction for fib Sort Prop.
Print fib_ind.

Function fi (n:nat) : nat :=
  match n with
    0 => 1
  | 1 => 1
  | S ((S p) as q) => fi p + fi q
  end.

Check (fi_ind, fib_ind).

Theorem fib_ind' :
  forall P : nat -> Prop,
    P 0 -> P 1 ->
    (forall n, P n -> P (S n) -> P (S (S n)))->
    forall n, P n.
Proof.
 intros.
 pattern n, (fib n).
 apply fib_ind.
 info auto.
 info auto.
 intros; subst; info auto.
 Show Proof.
(*
 intros P H0 H1 Hstep n.
 assert (P n/\P(S n)).
 elim n; intuition.
 intuition.
*)
Qed.