def ms_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addb.bend:58

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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adds.bend as AS

58def ms_le(+one: Nat, +h1: {one == 1n : Nat}, +Fl: Nat, +m: Nat, +d: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hd: {Nat.is_le(1n, d) == True{} : Bool}) -> {Nat.is_le(m, C.shift(d, Nat.add(Fl, C.shift(52n, one)))) == True{} : Bool}:
59  +P53 = C.shift(53n, one)
60  +h1a = N.lt_le(m, P53, Equal.trans(Bool, Nat.is_lt(m, P53), C.fits(53n, m), True{}, FR.lt_fit(53n, one, h1, m), hm))
61  +h2 = L.subst(Nat, z => {Nat.is_le(z, C.shift(1n, Nat.add(Fl, C.shift(52n, one)))) == True{} : Bool}, C.shift(1n, C.shift(52n, one)), P53, Equal.sym(Nat, P53, C.shift(1n, C.shift(52n, one)), WW.shift_comp(1n, 52n, one)), WW.shift_mono(1n, C.shift(52n, one), Nat.add(Fl, C.shift(52n, one)), L.subst(Nat, z => {Nat.is_le(C.shift(52n, one), z) == True{} : Bool}, Nat.add(C.shift(52n, one), Fl), Nat.add(Fl, C.shift(52n, one)), NA.add_comm(C.shift(52n, one), Fl), N.le_add_right(C.shift(52n, one), Fl))))
62  N.le_trans(m, P53, C.shift(d, Nat.add(Fl, C.shift(52n, one))), h1a, N.le_trans(P53, C.shift(1n, Nat.add(Fl, C.shift(52n, one))), C.shift(d, Nat.add(Fl, C.shift(52n, one))), h2, AS.shmk(1n, d, Nat.add(Fl, C.shift(52n, one)), hd)))