def xem

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:81

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as F64addf
import 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), {==})

Uses (6)

Used by (1)