Induction base case (source code)

= Induction base case
{title2=$P(n_0)$}

The starting instance of a <mathematical induction> proof, established directly before the <inductive step> is applied. The implication $P(n)\Rightarrow P(n+1)$ alone can be true when every instance is false. For example, $\sum_{j=1}^n j=n(n+1)/2+C$ with $C\ne0$ has a formally correct successor calculation but a false base case.