def plus1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/montnat.bend:54

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

54def plus1(+x: Nat) -> {Nat.add(x, 1n) == 1n+x : Nat}:
55  Equal.trans(Nat, Nat.add(x, 1n), 1n+Nat.add(x, 0n), 1n+x, N.add_succ(x, 0n), N.succ_cong(Nat.add(x, 0n), x, N.add_zero(x)))