Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

q,n:. (qn)

Applied Tactic: UnivCD THENW Auto THEN NatInd 2 THEN RecCaseSplit `geom_series` THENA Auto
Generated subgoals:

1. 0

2. (q-1) + (q-1)

3. 0

4. (qn - 1) + (qn - 1)