def half_hi

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqn.bend:69

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/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/arith.bend as NR

69def half_hi(+S: Nat, +n: Nat, +h: {Nat.is_le(n, Nat.add(13n, Nat.add(S, S))) == True{} : Bool}) -> {Nat.is_le(Nat.div(n, 2n), Nat.add(6n, S)) == True{} : Bool}:
70  +e = Equal.trans(Nat, Nat.mul(Nat.add(7n, S), 2n), Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(14n, Nat.add(S, S)), two_mul(Nat.add(7n, S)), Equal.trans(Nat, Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(S, Nat.add(S, 14n)), Nat.add(14n, Nat.add(S, S)), Equal.trans(Nat, Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(Nat.add(S, 7n), Nat.add(S, 7n)), Nat.add(S, Nat.add(S, 14n)), Equal.trans(Nat, Nat.add(Nat.add(7n, S), Nat.add(7n, S)), Nat.add(Nat.add(S, 7n), Nat.add(7n, S)), Nat.add(Nat.add(S, 7n), Nat.add(S, 7n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(7n, S)), Nat.add(7n, S), Nat.add(S, 7n), Equal.trans(Nat, Nat.add(7n, S), Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, 7n), Equal.cong(Nat, Nat, z => Nat.add(7n, z), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.trans(Nat, Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, Nat.add(7n, 0n)), Nat.add(S, 7n), NA.add_swap(7n, S, 0n), {==}))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, 7n), z), Nat.add(7n, S), Nat.add(S, 7n), Equal.trans(Nat, Nat.add(7n, S), Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, 7n), Equal.cong(Nat, Nat, z => Nat.add(7n, z), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.trans(Nat, Nat.add(7n, Nat.add(S, 0n)), Nat.add(S, Nat.add(7n, 0n)), Nat.add(S, 7n), NA.add_swap(7n, S, 0n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(S, 7n), Nat.add(S, 7n)), Nat.add(S, Nat.add(7n, Nat.add(S, 7n))), Nat.add(S, Nat.add(S, 14n)), NA.add_assoc(S, 7n, Nat.add(S, 7n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(7n, Nat.add(S, 7n)), Nat.add(S, 14n), Equal.trans(Nat, Nat.add(7n, Nat.add(S, 7n)), Nat.add(S, Nat.add(7n, 7n)), Nat.add(S, 14n), NA.add_swap(7n, S, 7n), {==})))), Equal.sym(Nat, Nat.add(14n, Nat.add(S, S)), Nat.add(S, Nat.add(S, 14n)), Equal.trans(Nat, Nat.add(14n, Nat.add(S, S)), Nat.add(14n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 14n)), Equal.cong(Nat, Nat, z => Nat.add(14n, z), Nat.add(S, S), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(S, 0n)), Equal.trans(Nat, Nat.add(S, S), Nat.add(Nat.add(S, 0n), S), Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, S), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(S, 0n), z), S, Nat.add(S, 0n), Equal.sym(Nat, Nat.add(S, 0n), S, N.add_zero(S)))), Equal.trans(Nat, Nat.add(Nat.add(S, 0n), Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 0n)), NA.add_assoc(S, 0n, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(S, 0n)), Nat.add(S, Nat.add(0n, 0n)), Nat.add(S, 0n), NA.add_swap(0n, S, 0n), {==}))))), Equal.trans(Nat, Nat.add(14n, Nat.add(S, Nat.add(S, 0n))), Nat.add(S, Nat.add(14n, Nat.add(S, 0n))), Nat.add(S, Nat.add(S, 14n)), NA.add_swap(14n, S, Nat.add(S, 0n)), Equal.cong(Nat, Nat, z => Nat.add(S, z), Nat.add(14n, Nat.add(S, 0n)), Nat.add(S, 14n), Equal.trans(Nat, Nat.add(14n, Nat.add(S, 0n)), Nat.add(S, Nat.add(14n, 0n)), Nat.add(S, 14n), NA.add_swap(14n, S, 0n), {==})))))))
71  +l1 = N.le_lt_succ(n, Nat.add(13n, Nat.add(S, S)), h)
72  +l2 = Equal.trans(Bool, Nat.is_le(Nat.add(7n, S), Nat.div(n, 2n)), Nat.is_le(Nat.mul(Nat.add(7n, S), 2n), n), False{}, NR.le_div(1n, Nat.add(7n, S), n), L.subst(Nat, z => {Nat.is_le(z, n) == False{} : Bool}, Nat.add(14n, Nat.add(S, S)), Nat.mul(Nat.add(7n, S), 2n), Equal.sym(Nat, Nat.mul(Nat.add(7n, S), 2n), Nat.add(14n, Nat.add(S, S)), e), N.lt_not_le(n, Nat.add(14n, Nat.add(S, S)), l1)))
73  N.lt_succ_le(Nat.div(n, 2n), Nat.add(6n, S), N.not_le_lt(Nat.add(7n, S), Nat.div(n, 2n), l2))