def strict_le

stelliferous@0.0.2.0 · proofs/nat_to_u32_bounds.bend:18

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

18def strict_le(+a: Nat,+b: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_le(a,b) == True{} : Bool}:
19  match a b:
20    case 0n 0n:
21      {==}
22    case 0n 1n+bp:
23      {==}
24    case 1n+ap 0n:
25      Empty.absurd({Nat.is_le(1n+ap,0n) == True{} : Bool},WordEncoding.false_true(h))
26    case 1n+ap 1n+bp:
27      strict_le(ap,bp,h)