Induction on two integer variables

Here are some induction principles for two variables:

• $P(0,0)$
• $\forall x,y. P(x,y) \Rightarrow P(x+1,y)$

• $\forall x,y. P(x,y) \Rightarrow P(x,y+1)$

  ---

• $\forall x,y. P(x,y)$

and

• $P(0,0)$
• $\forall x,y. P(x,0) \Rightarrow P(x+1,0)$

• $\forall x,y. P(x+1,y) \Rightarrow P(x,y+1)$

  ---

• $\forall x,y. P(x,y)$

Suppose you are trying to prove a family of statements $P(x, y)$. This is the same as proving the family of statements $F(x)$, where $F(x) = \forall y : P(x, y)$. Each statement $F(x)$ can be proven by induction on $y$ (for fixed $x$), and then you can prove $P(x, y)$ by induction on $x$. You might want to try proving

$${n+1 \choose k+1} = {n \choose k+1} + {n \choose k}$$

this way.

But actually you can be much trickier than this. Sometimes it suffices to induct on $x + y$, for example.