车削一个<= b键SUC一个<= SUC b

Question

这是问题的扩展张贴在这里：

Agda and Binary Search Trees

我有

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

用于trans₁定义，但这需要我将下面的加宽的定义更改为：

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构造函数的小于或等于关系。请在课程论坛上询问，而不是堆栈溢出。