def hx

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64ofnat.bend:25

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

25def hx(+bb: Nat) -> {Nat.add(Nat.add(2937n, bb), 2180n) == Nat.add(5117n, bb) : Nat}:
26  Equal.trans(Nat, Nat.add(Nat.add(2937n, bb), 2180n), Nat.add(2937n, Nat.add(bb, 2180n)), Nat.add(5117n, bb), NA.add_assoc(2937n, bb, 2180n), Equal.cong(Nat, Nat, z => Nat.add(2937n, z), Nat.add(bb, 2180n), Nat.add(2180n, bb), NA.add_comm(bb, 2180n)))