def sub_sub_self

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/fact.bend:219

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A

219# n - (n - k) == k for k <= n
220def sub_sub_self(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.sub(n, Nat.sub(n, k)) == k : Nat}:
221  +e = N.sub_add(n, k, h)
222  %Equal.sym(Nat, n, Nat.add(k, Nat.sub(n, k)), Equal.sym(Nat, Nat.add(k, Nat.sub(n, k)), n, e)) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
223  %Equal.sym(Nat, Nat.add(k, Nat.sub(n, k)), Nat.add(Nat.sub(n, k), k), A.add_comm(k, Nat.sub(n, k))) : {Nat.sub(_, Nat.sub(n, k)) == k : Nat}
224  N.add_sub_cancel(Nat.sub(n, k), k)