I have been wondering if the following equivalence holds:
$(\forall i \, | \, 0 \leq i \leq n : f.i \leq f.n) \, \land \, f.n \leq f.(n+1) \equiv (\forall i \, | \, 0 \leq i \leq n + 1 : f.i \leq f.(n+1))$
So, I try to prove the $\Rightarrow$ direction by distributivity of $\land$ over $\forall$, and then by transitivity of $\leq$, but this gets me to:
$(\forall i \, | \, 0 \leq i \leq n : f.i \leq f.(n+1))$
I believe that this is equivalent to the consequent I am trying to establish, however, I don't I know of a rule that allows me to expand the range of the quantification to include $n+1$.
By the way, I am using the rules of the predicate calculus according to the book "A Logical Approach to Discrete Math", by Gries and Schnedier.
You need your logic to somehow recognize the equivalence $$ ((0 \leq i \land i \leq n) \lor i = n + 1) \iff (0 \leq i \land i \leq n + 1). $$ Without some kind of rules about how natural numbers function, this will not work. Just the rules of predicate logic, together with, say, the axioms of a partial/total ordering, are not enough. For instance, the sentence does not hold if the letter $i$ ranges over all real numbers.