proofs/math/typed/f64divx.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divx.bend as F64divx

import Base
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR

Definitions

@+dp:Nat -> @+P:Nat -> @+u:Nat -> @+K:Nat -> @+sx:Nat -> @+sy:Nat -> @+hc:{Nat.add(dp, P) == 200n : Nat} -> @+hb:{Nat.add(62n, u) == Nat.add(sy, P) : Nat} -> @+hf:{Nat.add(u, K) == Nat.add(sx, 1022n) : Nat} -> {Nat.add(sx, Nat.add(dp, 884n)) == Nat.add(sy, K) : Nat}

@+E:Nat -> @+XX:Nat -> @+XY:Nat -> @+dp:Nat -> @+P:Nat -> @+u:Nat -> @+K:Nat -> @+sx:Nat -> @+sy:Nat -> @+EA:Nat -> @+EB:Nat -> @+e:Nat -> @+ha:{Nat.add(E, Nat.add(XY, 201n)) == Nat.add(XX, 3000n) : Nat} -> @+hc:{Nat.add(dp, P) == 200n : Nat} -> @+hb:{Nat.add(62n, u) == Nat.add(sy, P) : Nat} -> @+hf:{Nat.add(u, K) == Nat.add(sx, 1022n) : Nat} -> @+hEAx:{Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat} -> @+hEBy:{Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat} -> @+hd:{Nat.add(e, EB) == Nat.add(EA, Nat.add(4096n, K)) : Nat} -> {Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n) == e : Nat}