Usage of "also have...finally have" in Isabelle

Question

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?

Answer 1

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.