~/jendhub

law sv_lt_j

lawful-bytes@0.1.1.0 · proof_shift.bend:197

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

197law sv_lt_j:
198  for +jj: Nat
199  for +kk: Nat
200  for +n: Nat
201  for +ll: Nat
202  for +hm: {Nat.add(Nat.add(jj, kk), 1n+n) == ll : Nat}
203  {Nat.is_lt(jj, ll) == True{} : Bool}

Uses (7)

Used by (1)