I usually think of also have as working like this:
have "P r Q1" by simp
also have "... r Q2" by simp
also have "... r Q3" by simp
...
also have "... r Qn" by simp
finally have "P r Qn+1" by simp
where "... r Qm" means "Qm-1 r Qm" and r is some transitive relation.
With r meaning = this seems to really be the case, however, when using ≥ I have found a counterexample to this description:
...
have "1- 1/(2^(n+1))≥1/(2::real)" by simp
also have "... ≥ 0" (* here when I check the 'output' it seems to be
considering "0 ≤ 1 - 1 / 2 ^ (n + 1)" which in the previous notation
would be Qn r Qn+2 !*)
My question is, how does also have work, in particular, how do I predict what ... is going to refer to?
AFAIR, a ≥ b is an abbreviation for b ≤ a. With this in mind, you see that this does not fit the pattern expected by also.
I suggest that you state your chain of inequations the other way, from lowest to highest. You can still state the final result using ≥ if you want – after all, it is just an abbreviation.