def wn.le_add_l

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

import Base

164def wn.le_add_l(k: Nat, -x: Nat, -y: Nat) -> {Nat.is_le(Nat.add(k, x), Nat.add(k, y)) == Nat.is_le(x, y) : Bool}:
165  match k:
166    case 0n:
167      {==}
168    case 1n+p:
169      wn.le_add_l(p, x, y)