def root_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:211

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/math/typed/u32.bend as U32P

211# r^2 <= n < (s + 1)^2 gives r <= s
212def root_le(+r: Nat, +s: Nat, +n: Nat, +hr: {Nat.is_le(sq(r), n) == True{} : Bool}, +hs: {Nat.is_lt(n, sq(1n+s)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(s, r) == c : Bool}) -> {Nat.is_le(r, s) == True{} : Bool}:
213  match c:
214    case False{}:
215      N.not_lt_le(s, r, hc)
216    case True{}:
217      +le = sq_mono(1n+s, r, N.lt_succ_le_succ(s, r, hc))
218      +nn = N.lt_le_trans(n, sq(1n+s), n, hs, N.le_trans(sq(1n+s), sq(r), n, le, hr))
219      Empty.absurd({Nat.is_le(r, s) == True{} : Bool}, U32P.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(n, n), False{}, Equal.sym(Bool, Nat.is_lt(n, n), True{}, nn), N.lt_irrefl(n))))