law sv_lt

lawful-bytes@0.1.1.0 · proof_shift.bend:183

import Base

183# Nat facts for one step: j + k + (1 + n) = L.
184law sv_lt:
185  for +jj: Nat
186  for +kk: Nat
187  for +n: Nat
188  for +ll: Nat
189  for +hm: {Nat.add(Nat.add(jj, kk), 1n+n) == ll : Nat}
190  {Nat.is_lt(Nat.add(jj, kk), ll) == True{} : Bool}