def na.lt_le

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:177

import Base

177def na.lt_le(+a: Nat, +b: Nat) -> {Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}:
178  match a b:
179    case 0n 0n:
180      h => bo.absurd({Nat.is_le(0n, 0n) == True{} : Bool}, h)
181    case 0n 1n+bp:
182      h => {==}
183    case 1n+ap 0n:
184      h => bo.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, h)
185    case 1n+ap 1n+bp:
186      h => na.lt_le(ap, bp)(h)