Fix PR2002. Suppose n is the initial value for the induction