test-suite/bugs/closed/2602.v


1
2
3
4
5
6
7
8

Goal exists m, S m > 0.
eexists.
match goal with
 | |- context [ S ?a ] =>
     match goal with
       | |- S a > 0 => idtac
     end
end.