Turning a <= b to suc a <= suc b
Question
This is an extension of the question posted here:
I have
trans₁ : ∀ {a b c} → suc a ≤ suc b → suc b ≤ c → suc a ≤ c
for the definition of trans₁
, but this would require me to change the definition of widen below to:
widen : ∀{min max newMin newMax}
→ BST min max
→ suc newMin ≤ suc min
→ max ≤ newMax
→ BST newMin newMax
How would i change a <= b
to suc a <= suc b
? This would then allow me to change the definition of trans₁
to:
trans₁ : ∀ {a b c} → a ≤ b → suc b ≤ c → suc a ≤ c
Any help is greatly appreciated.
Solution
Look at the s<=s constructor for the less than or equal to relation. Please ask on the course forums, not on stack overflow.
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow