def mid_lt_hi

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/roots.bend:80

import Base
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/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

80# lo < hi gives (lo + hi) / 2 < hi
81def mid_lt_hi(+lo: Nat, +hi: Nat, +h: {Nat.is_lt(lo, hi) == True{} : Bool}) -> {Nat.is_lt(M.mid(lo, hi), hi) == True{} : Bool}:
82  +e = Equal.trans(Bool, Nat.is_le(hi, M.mid(lo, hi)), Nat.is_le(Nat.mul(hi, 2n), Nat.add(lo, hi)), False{}, R.le_div(1n, hi, Nat.add(lo, hi)),
83    Equal.trans(Bool, Nat.is_le(Nat.mul(hi, 2n), Nat.add(lo, hi)), Nat.is_le(Nat.add(hi, hi), Nat.add(hi, lo)), False{},
84      Equal.trans(Bool, Nat.is_le(Nat.mul(hi, 2n), Nat.add(lo, hi)), Nat.is_le(Nat.add(hi, hi), Nat.add(lo, hi)), Nat.is_le(Nat.add(hi, hi), Nat.add(hi, lo)), Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(lo, hi)), Nat.mul(hi, 2n), Nat.add(hi, hi), two_mul(hi)), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(hi, hi), z), Nat.add(lo, hi), Nat.add(hi, lo), A.add_comm(lo, hi))),
85      Equal.trans(Bool, Nat.is_le(Nat.add(hi, hi), Nat.add(hi, lo)), Nat.is_le(hi, lo), False{}, R.le_add_cancel(hi, hi, lo), N.lt_not_le(lo, hi, h))))
86  N.not_le_lt(hi, M.mid(lo, hi), e)