def two62

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqr.bend:104

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/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/natural/sqrtn.bend as SQ2
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

104def two62(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(2n, C.shift(62n, one)) == True{} : Bool}:
105  +h = L.subst(Nat, o => {Nat.is_le(o, C.shift(61n, one)) == True{} : Bool}, one, 1n, h1, WW.shift_ge(61n, one))
106  L.subst(Nat, z => {Nat.is_le(2n, z) == True{} : Bool}, Nat.add(C.shift(61n, one), C.shift(61n, one)), C.shift(62n, one), Equal.sym(Nat, C.shift(62n, one), Nat.add(C.shift(61n, one), C.shift(61n, one)), NA.double_self(C.shift(61n, one))), SQ2.le_add2(1n, C.shift(61n, one), 1n, C.shift(61n, one), h, h))