Coq中的Defintion和'Let'有什么区别？为什么有些定义需要证明？例如.这是集团理论中g1.v的一段代码.
Definition exp : Z -> U -> U.
Proof.
intros n a.
elim n; clear n.
exact e.
intro n.
elim n; clear n.
exact a.
intros n valrec.
exact (star a valrec).
intro n; elim n; clear n.
exact (inv a).
intros n valrec.
exact (star (inv a) valrec).
Defined.
这个证明的目的是什么？