def sub_add_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:734

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 NA

734def sub_add_l(+a: Nat, +x: Nat) -> {Nat.sub(Nat.add(a, x), x) == a : Nat}:
735  Equal.trans(Nat, Nat.sub(Nat.add(a, x), x), Nat.sub(Nat.add(x, a), x), a, Equal.cong(Nat, Nat, z => Nat.sub(z, x), Nat.add(a, x), Nat.add(x, a), NA.add_comm(a, x)), N.add_sub_cancel(x, a))