def xem
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as F64addfimport Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG
81def xem(+e: Nat) -> {Nat.add(1926n, Nat.sub(e, 1n)) == AG.xe(e) : Nat}:
82 xem_c(e, Nat.is_eq(e, 0n), {==})