def na.lt_le

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:292

import Base

292def na.lt_le(+a: Nat, +b: Nat) -> {Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}:
293  match a b:
294    case 0n 0n:
295      h => bo.absurd({Nat.is_le(0n, 0n) == True{} : Bool}, h)
296    case 0n 1n+bp:
297      h => {==}
298    case 1n+ap 0n:
299      h => bo.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, h)
300    case 1n+ap 1n+bp:
301      h => na.lt_le(ap, bp)(h)