Sqrtn.step_lt: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as Sqrtn Lines 89-114 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend&start_line=89&end_line=114 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 import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as B def step_lt(+n: Nat, +gp: Nat, +m: Nat, +hm: {m == M.sqrt_next(n, 1n+gp) : Nat}) -> {Nat.is_lt(n, Nat.mul(1n+m, 1n+m)) == True{} : Bool}: +g = {1n+gp : Nat} +q = Nat.div(n, g) +r = Nat.mod(n, g) +s = Nat.add(g, q) # n < g (q + 1) +ha = Equal.trans(Bool, Nat.is_lt(n, Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.add(Nat.mul(q, g), g)), True{}, Equal.trans(Bool, Nat.is_lt(n, Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.add(Nat.mul(q, g), g)), Equal.cong(Nat, Bool, z => Nat.is_lt(z, Nat.mul(g, 1n+q)), n, Nat.add(Nat.mul(q, g), r), R.dm_eq(gp, n)), Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(Nat.mul(q, g), r), z), Nat.mul(g, 1n+q), Nat.add(Nat.mul(q, g), g), Equal.trans(Nat, Nat.mul(g, 1n+q), Nat.mul(1n+q, g), Nat.add(Nat.mul(q, g), g), A.mul_comm(g, 1n+q), A.add_comm(g, Nat.mul(q, g))))), N.lt_add_left(r, g, Nat.mul(q, g), R.dm_lt(gp, n))) # g + (q + 1) <= 2 (m + 1): s == 2 m + (s mod 2) +es = Equal.trans(Nat, s, Nat.add(Nat.double(m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), Equal.trans(Nat, s, Nat.add(Nat.double(Nat.div(s, 2n)), Nat.mod(s, 2n)), Nat.add(Nat.double(m), Nat.mod(s, 2n)), B.half_eq(s), Equal.cong(Nat, Nat, z => Nat.add(Nat.double(z), Nat.mod(s, 2n)), Nat.div(s, 2n), m, Equal.sym(Nat, m, Nat.div(s, 2n), hm))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(s, 2n)), Nat.double(m), Nat.add(m, m), A.double_self(m))) +hs = Equal.trans(Bool, Nat.is_le(s, 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), 1n)), True{}, Equal.trans(Bool, Nat.is_le(s, 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), 1n)), Equal.cong(Nat, Bool, z => Nat.is_le(z, 1n+Nat.add(m, m)), s, Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), es), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), z), 1n+Nat.add(m, m), Nat.add(Nat.add(m, m), 1n), A.add_comm(1n, Nat.add(m, m)))), N.le_add_left(Nat.mod(s, 2n), 1n, Nat.add(m, m), N.lt_succ_le(Nat.mod(s, 2n), 1n, B.half_rem(s)))) +hb = Equal.trans(Bool, Nat.is_le(Nat.add(g, 1n+q), Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, 2n+Nat.add(m, m)), True{}, Equal.trans(Bool, Nat.is_le(Nat.add(g, 1n+q), Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, 2n+Nat.add(m, m)), Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(1n+m, 1n+m)), Nat.add(g, 1n+q), 1n+s, A.add_succ(g, q)), Equal.cong(Nat, Bool, z => Nat.is_le(1n+s, z), Nat.add(1n+m, 1n+m), 2n+Nat.add(m, m), add_two(m, m))), hs) N.lt_le_trans(n, Nat.mul(g, 1n+q), Nat.mul(1n+m, 1n+m), ha, prod_le(g, 1n+q, 1n+m, hb)) Uses (27): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_add_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend&name=half_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend&name=half_rem https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend&name=add_two https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend&name=prod_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=sqrt_next