fact: Fixpoint fib_positive (p:positive) : {u:nat & { v : nat | u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))}} := match p return {u:nat & { v : nat | u = fib (nat_of_P p) /\ v = fib (S (nat_of_P p))}} with xH => (existT (fun u=> { v : nat | u = 1 /\ v = 2}) 1 (exist (fun v => 1 = 1 /\ v = 2) 2 (conj (refl_equal 1) (refl_equal 2)))) | xI p' => match fib_positive p' with (existT _ u (exist _ v h)) => (existT (fun u => { v: nat | u = fib (nat_of_P (xI p')) /\ v = fib (S (nat_of_P (xI p')))}) (2*u*v - u*u) (exist (fun w=> 2*u*v-u*u = fib (nat_of_P (xI p')) /\ w= fib (S (nat_of_P (xI p')))) (v*v + u*u) (th_fib_positive1 p' u v h))) end | xO p' => match fib_positive p' with (existT _ u (exist _ v h)) => (existT (fun u => { v: nat | u = fib (nat_of_P (xO p')) /\ v = fib (S (nat_of_P (xO p')))}) (u*u+(v-u)*(v-u)) (exist (fun w => u*u+(v-u)*(v-u) = fib (nat_of_P (xO p'))/\ w = fib (S (nat_of_P (xO p')))) (2*u*v-u*u) (th_fib_positive0 p' u v h))) end end.
imports: Arith ArithRing ZArith fib_ind OldArith