def ilt_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqa.bend:43

import Base
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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

43def ilt_c(+n: Nat, +s: Nat, +h: {Nat.is_lt(n, Nat.mul(s, s)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(M.isqrt(n), s) == c : Bool}) -> {c == True{} : Bool}:
44  match c:
45    case True{}:
46      {==}
47    case False{}:
48      +l1 = N.not_lt_le(M.isqrt(n), s, hc)
49      +l2 = N.le_trans(Nat.mul(s, s), Nat.mul(M.isqrt(n), M.isqrt(n)), n, sqmono(s, M.isqrt(n), l1), isl(n))
50      NC.absurd_tf({False{} == True{} : Bool}, Equal.trans(Bool, False{}, Nat.is_le(Nat.mul(s, s), n), True{}, Equal.sym(Bool, Nat.is_le(Nat.mul(s, s), n), False{}, N.lt_not_le(n, Nat.mul(s, s), h)), l2))