~/jendhub

law sv_jk1

lawful-bytes@0.1.1.0 · proof_shift.bend:223

import lawful-bytes@0.1.1.0/proof_shift.bend as ProofShift
import Base

223law sv_jk1:
224  for +jj: Nat
225  for +kk: Nat
226  for +ll: Nat
227  for +h: {Nat.is_lt(Nat.add(jj, kk), ll) == True{} : Bool}
228  {Nat.is_le(Nat.add(Nat.add(jj, 1n), kk), ll) == True{} : Bool}

Uses (10)

Used by (1)