def ud.lt_add

bend-osdev-u32@0.1.0.0 · PROOF_div.bend:97

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

97def ud.lt_add(+m: Nat, +r: Nat) -> {Nat.is_lt(r, 1n+Nat.add(m, r)) == True{} : Bool}:
98  match r:
99    case 0n:
100      {==}
101    case 1n+p:
102      %Equal.sym(Nat, Nat.add(m, 1n+p), 1n+Nat.add(m, p), UL.nat_add_succ(m, p)) : {Nat.is_lt(1n+p, 1n+_) == True{} : Bool}
103      ud.lt_add(m, p)