equality - 将 a <= b 转换为 suc a <= suc b

Question

这是此处发布的问题的扩展:

Agda and Binary Search Trees

我有

trans₁ : ∀ {a b c} → suc a ≤ suc b → suc b ≤ c → suc a ≤ c

对于trans₁的定义，但这需要我将下面的 widen 定义更改为:

widen : ∀{min max newMin newMax}
      → BST min max
      → suc newMin ≤ suc min
      → max ≤ newMax
      → BST newMin newMax

我将如何更改 a <= b至 suc a <= suc b ？这将允许我更改 trans₁ 的定义到:

trans₁ : ∀ {a b c} → a ≤ b → suc b ≤ c → suc a ≤ c

非常感谢任何帮助。

Answer 1

查看小于或等于关系的 s<=s 构造函数。请在类(class)论坛上提问，而不是在堆栈溢出上提问。