proposition: Theorem fib_monotonic : forall n, fib n <= fib (n+1).
proof: Proof. intros n; elim n using fib_ind; auto with arith. intros n' H1 H2; replace (S (S n')+1) with (S (S (S n'))) by ring. rewrite (fib_SSn (S n')); auto with arith. Qed.
imports: Arith ArithRing ZArith fib_ind OldArith