How to switch the current target in Coq?

Question

Is it possible to switch the current target or subgoal to prove in Coq?

For example, I have a goal like this (from eexists):

______________________________________(1/1) ?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2) 

What I want to do is split and first prove the correct conjunction. This, I think, will give the value of the existential variable ?s , and the left conjunction should just be a simplification.

But split by default sets the left conjunctive ?s > 0 as the current target.

 ______________________________________(1/2) ?s > 0 ______________________________________(2/2) r1 * (r1 + s1) + ?s = r3 * (r3 + s2) 

I know that I can attribute tactics 2: to work in the second subgoal, but this is inconvenient because

1) I do not see hypotheses for goal number 2 and

2) if it is in a different context, goal number 2 may be the third or k_th goal. The evidence will not be portable.

That is why I want to set the second goal as current.

By the way, I am using CoqIDE (8.5).

Answer 1

You can use Focus 2 to focus on the second target.