def half_bound

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:379

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/lemmas/proofs/nat_algebra.bend as NA

379# a (1 + kp) < 2^g from a (2 + 2 kp) < 2^(1 + g)
380def half_bound(+a: Nat, +kp: Nat, +g: Nat, +hb: {Nat.is_lt(Nat.mul(a, Nat.double(1n+kp)), C.pow2(1n+g)) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, 1n+kp), C.pow2(g)) == True{} : Bool}:
381  +e = Equal.trans(Nat, Nat.mul(a, Nat.double(1n+kp)), Nat.mul(Nat.double(1n+kp), a), Nat.double(Nat.mul(1n+kp, a)), NA.mul_comm(a, Nat.double(1n+kp)), dmul(1n+kp, a))
382  double_lt_inv(Nat.mul(a, 1n+kp), C.pow2(g), Equal.trans(Bool, Nat.is_lt(Nat.double(Nat.mul(a, 1n+kp)), Nat.double(C.pow2(g))), Nat.is_lt(Nat.mul(a, Nat.double(1n+kp)), Nat.double(C.pow2(g))), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.double(C.pow2(g))), Nat.double(Nat.mul(a, 1n+kp)), Nat.mul(a, Nat.double(1n+kp)), Equal.sym(Nat, Nat.mul(a, Nat.double(1n+kp)), Nat.double(Nat.mul(a, 1n+kp)), Equal.trans(Nat, Nat.mul(a, Nat.double(1n+kp)), Nat.double(Nat.mul(1n+kp, a)), Nat.double(Nat.mul(a, 1n+kp)), e, Equal.cong(Nat, Nat, t => Nat.double(t), Nat.mul(1n+kp, a), Nat.mul(a, 1n+kp), NA.mul_comm(1n+kp, a))))), hb))