小编Jef*_*rey的帖子

我想在Coq中证明:

convert l' + 1 + (convert l' + 1) = convert l' + convert l' + 1 + 1

只有一些括号是多余的,不要让我使用reflexivity命令; 所以我该怎么做？

所有元素都是nat(自然)类型,因为这convert l'是一个返回nat数的函数,我不想使用像Omega这样的强大策略等等.