Level: Lib Thy Top: 1
Hypotheses:

  1. n :

Conclusion:

n * n + 1

Applied Tactic: MemTypeCD THENM Auto THENW Auto
Generated subgoals:

1. 0 n * n + 1