fact: Definition fib_log_F: forall (x : nat), (forall (y : nat), y < x -> ({u : nat & {v : nat | u = fib y /\ v = fib (S y)}})) -> ({u : nat & {v : nat | u = fib x /\ v = fib (S x)}}).
imports: Arith ArithRing Wf_nat fib_ind fib_positive Lia