def fsub_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:558

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/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH

558def fsub_c(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +R0: Nat, +hR: {Nat.is_le(R0, C.shift(1n+k, one)) == True{} : Bool}, +f: Bool, +hf: {C.fits(1n+k, R0) == f : Bool}) -> {C.fits(1n+k, Nat.sub(R0, Nat.mod(R0, 2n))) == f : Bool}:
559  match f:
560    case True{}:
561      SH.fits_lek(1n+k, Nat.sub(R0, Nat.mod(R0, 2n)), R0, UH.sub_le(R0, Nat.mod(R0, 2n)), hf)
562    case False{}:
563      +hlt = Equal.trans(Bool, Nat.is_lt(R0, C.shift(1n+k, one)), C.fits(1n+k, R0), False{}, lt_fit(1n+k, one, h1, R0), hf)
564      +eR = N.le_antisym(R0, C.shift(1n+k, one), hR, N.not_lt_le(R0, C.shift(1n+k, one), hlt))
565      +em = Equal.trans(Nat, Nat.mod(R0, 2n), Nat.mod(C.shift(1n+k, one), 2n), 0n, Equal.cong(Nat, Nat, z => Nat.mod(z, 2n), R0, C.shift(1n+k, one), eR), mod_sh(k, one))
566      +es = Equal.trans(Nat, Nat.sub(R0, Nat.mod(R0, 2n)), Nat.sub(R0, 0n), R0, Equal.cong(Nat, Nat, z => Nat.sub(R0, z), Nat.mod(R0, 2n), 0n, em), N.sub_zero(R0))
567      Equal.trans(Bool, C.fits(1n+k, Nat.sub(R0, Nat.mod(R0, 2n))), C.fits(1n+k, R0), False{}, Equal.cong(Nat, Bool, z => C.fits(1n+k, z), Nat.sub(R0, Nat.mod(R0, 2n)), R0, es), hf)