def not_lt_le

bendtorch-core@0.1.0.0 · src/storage/arith.bend:445

import Base

445def not_lt_le(+a: Nat, +b: Nat, h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.is_le(b, a) == True{} : Bool}:
446  match a:
447    case 0n:
448      match b:
449        case 0n:
450          {==}
451        case 1n+q:
452          Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, clash_true(h))
453    case 1n+p:
454      match b:
455        case 0n:
456          {==}
457        case 1n+q:
458          not_lt_le(p, q, h)