~/jendhub

def wn.cmp_add_l

bend-osdev-word64@0.1.1.0 · proof_value.bend:171

import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue
import Base

171def wn.cmp_add_l(k: Nat, -x: Nat, -y: Nat) -> {Nat.cmp(Nat.add(k, x), Nat.add(k, y)) == Nat.cmp(x, y) : Cmp}:
172  match k:
173    case 0n:
174      {==}
175    case 1n+p:
176      wn.cmp_add_l(p, x, y)

Uses (4)

Used by (1)