~/jendhub

law ends_arith

lawful-fields@0.1.1.0 · proof_list.bend:346

import lawful-fields@0.1.1.0/proof_list.bend as ProofList
import Base

346law ends_arith:
347  for +from: Nat
348  for +lp: Nat
349  for +lj: Nat
350  {Nat.add(Nat.add(Nat.add(from, lp), 1n), lj) == Nat.add(from, Nat.add(lp, 1n+lj)) : Nat}

Uses (6)

Used by (1)