Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
z:
. positive(z)
Applied Tactic:
Unfold `positive` 0 THEN Auto
Generated subgoals:
1
. Mono{i}(p,x.x = 1
p (x - 1) on
)
z:
. positive(z) 
z:. positive(z) 
p (x - 1) on )