~/jendhub

def plus1

bend-collections-laws-math@1.0.0.0 · proofs/math/random/proof_pcg.bend:48

import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_pcg.bend as ProofPcg
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

48def plus1(+x: Nat) -> {Nat.add(x, 1n) == 1n+x : Nat}:
49  Equal.trans(Nat, Nat.add(x, 1n), 1n+Nat.add(x, 0n), 1n+x, NA.add_succ(x, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(x, 0n), x, NA.add_zero(x)))

Uses (6)

Used by (1)