I have proofs for

1. P(0, 0)
2. P(0,n)->P(0, Sn)
3. P(m,0)->P(S m, 0)
4. P(m,n)->P(S m, S n).

How do I prove A for all values in Coq?

I tried two normal inductions, but it required P(m,n)->P(m, S n), which is not necessarily true.

Thank you.

I have proofs for

1. P(0, 0)
2. P(0,n)->P(0, Sn)
3. P(m,0)->P(S m, 0)
4. P(m,n)->P(S m, S n).

How do I prove A for all values in Coq?

I tried two normal inductions, but it required P(m, S n)->P(S m, S n), which is not necessarily true.

Thank you.

I have proofs for

1. P(0, 0)
2. P(0,n)->P(0, Sn)
3. P(m,0)->P(S m, 0)
4. P(m,n)->P(S m, S n).

How do I prove A for all values in Coq?

I tried normal induction, but it requires P(m,n)->P(m, S n), which is not necessarily true.

Thank you.

I have proofs for

1. P(0, 0)
2. P(0,n)->P(0, Sn)
3. P(m,0)->P(S m, 0)
4. P(m,n)->P(S m, S n).

How do I prove A for all values in Coq?

I tried two normal inductions, but it required P(m,n)->P(m, S n), which is not necessarily true.

Thank you.