Level: Lib Thy Top: 1
Hypotheses:

  1. q :

  2. n :

Conclusion:

(qn + 1) = (qn) + (qn)

Applied Tactic: RW (AddrC [2](RecUnfoldC `geom_series`) ) 0THEN SplitOnConclITE THENA Auto
Generated subgoals:

1. 0 = (qn) + (qn)

2. (q(n + 1) - 1) + (q(n + 1) - 1) = (qn) + (qn)