def sub_z

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:108

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

108def sub_z(+a: Nat, +b: Nat, +h: {a == b : Nat}) -> {Nat.sub(a, b) == 0n : Nat}:
109  Equal.trans(Nat, Nat.sub(a, b), Nat.sub(b, b), 0n, Equal.cong(Nat, Nat, z => Nat.sub(z, b), a, b, h), N.sub_self(b))