F64next.per1: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend as F64next
Lines 210-217 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&start_line=210&end_line=217

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

# pat + 1 still fits 63 bits unless x is a NaN
def per1(+x: F.F64) -> {Nat.add(SF.pat(x), 1n) == Nat.add(Nat.add(SF.frac(x), 1n), C.shift(52n, SF.efield(x))) : Nat}:
  +Fr = SF.frac(x)
  +S = C.shift(52n, SF.efield(x))
  +ea = NA.add_assoc(Fr, S, 1n)
  +ec = Equal.cong(Nat, Nat, t => Nat.add(Fr, t), Nat.add(S, 1n), Nat.add(1n, S), NA.add_comm(S, 1n))
  +eb = Equal.sym(Nat, Nat.add(Nat.add(Fr, 1n), S), Nat.add(Fr, Nat.add(1n, S)), NA.add_assoc(Fr, 1n, S))
  Equal.trans(Nat, Nat.add(SF.pat(x), 1n), Nat.add(Fr, Nat.add(S, 1n)), Nat.add(Nat.add(Fr, 1n), S), ea, Equal.trans(Nat, Nat.add(Fr, Nat.add(S, 1n)), Nat.add(Fr, Nat.add(1n, S)), Nat.add(Nat.add(Fr, 1n), S), ec, eb))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=efield
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=frac
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64