如何在Coq中将两个项的小于关系转换为小于等于形式

首先明确前提：如果你公式中的S是皮亚诺算术中的后继函数（即S(n) = n + 1，且i1、i2均为自然数/整数），是可以转换为a1 ≤ a2形式的小于等于关系的，转换逻辑如下：

• 对于整数/自然数域的任意两个值x、y，严格小于关系x < y等价于x + 1 ≤ y
• 将原式S(i2) < i1代入上述规则，把x替换为S(i2)、y替换为i1，可得等价式：S(i2) + 1 ≤ i1，也就是S(S(i2)) ≤ i1
• 如果你需要把i2单独放在不等号左侧，也可以改写为i2 ≤ i1 - 2（该式仅在i1 ≥ 2的场景下成立，符合原式S(i2) < i1的约束，因为S(i2)最小为1，对应i1最小为2）

补充说明：如果你的S不是后继函数，需要明确S的定义才能给出准确的转换结果，但对于所有全序域的离散类型，x < y都可以转换为x + 最小步长 ≤ y的小于等于形式。

内容的提问来源于stack exchange，提问作者joshan beha