PrintForm Definitions exponent Sections AutomataTheory Doc

At: geom series limit 2 1 2

1. q:
2. a:
3. 0 < a
4. n:
5. (qn) a-1 < (qn+1)
6. a < (qn+1)

n:. (qn) a < (qn+1)

By: Witness n+1

Generated subgoal:

15. (qn)a-1
6. a-1 < (qn+1)
7. a < (qn+1)
a < (qn+1+1)


About:
existsaddnatural_numberintless_thansubtract