def sub_pos

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/roots.bend:124

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

124# lo < hi gives 0 < hi - lo
125def sub_pos(+lo: Nat, +hi: Nat, +h: {Nat.is_lt(lo, hi) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(hi, lo)) == True{} : Bool}:
126  match lo hi:
127    case lo0 0n:
128      Empty.absurd({Nat.is_lt(0n, Nat.sub(0n, lo0)) == True{} : Bool}, N.lt_zero_absurd(lo0, h))
129    case 0n 1n+hp:
130      {==}
131    case 1n+ +lp 1n+ +hp:
132      sub_pos(lp, hp, h)