def ns.sub_sub

bend-osdev-word64@0.1.1.0 · proof_shift.bend:62

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

62# k <= n: n - (n - k) = k
63def ns.sub_sub(+k: Nat, +n: Nat, h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.sub(n, Nat.sub(n, k)) == k : Nat}:
64  %ns.add_sub_le(k, n, h) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
65  P.wn.sub_add(k, Nat.sub(n, k))