def wn.lt_le

bend-osdev-word64@0.1.1.0 · proof_value.bend:136

import Base

136def wn.lt_le(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
137  match x y:
138    case 0n _:
139      wn.le_zero(y)
140    case 1n+xp 0n:
141      Empty.absurd({Nat.is_le(1n+xp, 0n) == True{} : Bool}, wn.ft(h))
142    case 1n+xp 1n+yp:
143      wn.lt_le(xp, yp, h)