def wn.lt_add_l

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

import Base

156# k + x < k + y, k + x <= k + y, cmp(k + x, k + y): as for x and y
157def wn.lt_add_l(k: Nat, -x: Nat, -y: Nat) -> {Nat.is_lt(Nat.add(k, x), Nat.add(k, y)) == Nat.is_lt(x, y) : Bool}:
158  match k:
159    case 0n:
160      {==}
161    case 1n+p:
162      wn.lt_add_l(p, x, y)