forward_for_simple_bound and EWD heuristic

[dnaumann]

forward_for_simple_bound recognizes the idiomatic pattern (init; i < hi; i++). People familiar with constructive program proving a la Dijkstra et al will write (init; i != hi; i++) when i has been introduced together with an invariant P(i) that generalizes a postcondition P(hi). Perhaps the tactic can be made to handle this pattern too, or at least to give a more helpful hint in this situation.