> E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your

> E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your goal to include something of the form n >= m -> P(n). The concept of a “minimal base case” really weirded me out but I couldn’t quite put my finger on why. Thanks for the painstaking explanation, this was perspective-broadening.