def ns.add_sub_le

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

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

58# k <= n: k + (n - k) = n
59def ns.add_sub_le(+k: Nat, +n: Nat, h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.add(k, Nat.sub(n, k)) == n : Nat}:
60  Equal.trans(Nat, Nat.add(k, Nat.sub(n, k)), Nat.add(Nat.sub(n, k), k), n, UL.nat_add_comm(k, Nat.sub(n, k)), UL.nat_le_witness(k, n, h))