def add_succ_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/lcm.bend:16

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

16def add_succ_zero(+b: Nat, +x: Nat, +e: {Nat.add(b, 1n+x) == 0n : Nat}) -> Empty:
17  N.succ_zero(Nat.add(b, x), Equal.trans(Nat, 1n+Nat.add(b, x), Nat.add(b, 1n+x), 0n, Equal.sym(Nat, Nat.add(b, 1n+x), 1n+Nat.add(b, x), A.add_succ(b, x)), e))