def gt.lt_self_add

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

import Base

140# x < 1 + (n + x)
141def gt.lt_self_add(+n: Nat, +x: Nat) -> {Nat.is_lt(x, 1n+Nat.add(n, x)) == True{} : Bool}:
142  match n:
143    case 0n:
144      gt.lt_self(x)
145    case 1n+k:
146      gt.lt_succ_r(x, 1n+Nat.add(k, x), gt.lt_self_add(k, x))