def add1c

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

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

484def add1c(+a: Nat, +k: Nat) -> {Nat.add(a, k) == Nat.add(k, a) : Nat}:
485  NA.add_comm(a, k)