def sub_add53

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:177

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

177def sub_add53(+X: Nat) -> {Nat.sub(Nat.add(X, 53n), 53n) == X : Nat}:
178  %Equal.sym(Nat, Nat.add(X, 53n), Nat.add(53n, X), N.add_comm(X, 53n)) : {Nat.sub(_, 53n) == X : Nat}
179  N.sub_zero(X)