自然数的定义为：

- O是自然数
- 自然数的后继是自然数

如0的后继为1,1的后继为2,...

定义等号运算符为：（参数为自然数a、b，返回一个bool）

- a为0，b为0：返回true
- a为a'的后继，b为b'的后继，返回(a'==b')//此处递归调用该运算符
- 其他情况：返回false

如何严谨地证明：对于任意自然数a，b，a==b返回值永远与b==a返回值相同？

如果能给出coq代码就更好了

Import Nat
Theorem a_eq_b：
forall a b:nat,a=?b = b=?a.
Proof.
(*填空*)
Qed.