Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
q,n,z.
(q
n
))
q:
n:
True
Applied Tactic:
ProveOpCombTyping `geom_series_wf`
Generated subgoals:
None