def gt.lt_add_left

bend-osdev-gf@0.1.1.0 · proof_tab.bend:148

import Base

148# b < n, so b < m + n
149def gt.lt_add_left(+m: Nat, +b: Nat, +n: Nat, +h: {Nat.is_lt(b, n) == True{} : Bool}) -> {Nat.is_lt(b, Nat.add(m, n)) == True{} : Bool}:
150  match m:
151    case 0n:
152      h
153    case 1n+k:
154      gt.lt_succ_r(b, Nat.add(k, n), gt.lt_add_left(k, b, n, h))