def k_hi_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqk.bend:58

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/f64sqa.bend as AQ
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as DM

58def k_hi_c(+X: Nat, +T: Nat, +S: Nat, +hlt: {Nat.is_lt(Nat.mul(S, S), Nat.add(Nat.mul(1n+T, 1n+T), Nat.add(Nat.add(T, T), Nat.add(T, T)))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(S, Nat.add(T, 2n)) == c : Bool}) -> {c == True{} : Bool}:
59  match c:
60    case True{}:
61      {==}
62    case False{}:
63      +h1 = N.lt_succ_le_succ(Nat.add(T, 2n), S, N.not_le_lt(S, Nat.add(T, 2n), hc))
64      +h2 = AQ.sqmono(Nat.add(1n+T, 2n), S, h1)
65      +h3 = N.lt_le_trans(Nat.mul(S, S), Nat.mul(Nat.add(1n+T, 2n), Nat.add(1n+T, 2n)), Nat.mul(S, S), N.lt_trans(Nat.mul(S, S), Nat.add(Nat.mul(1n+T, 1n+T), Nat.add(Nat.add(T, T), Nat.add(T, T))), Nat.mul(Nat.add(1n+T, 2n), Nat.add(1n+T, 2n)), hlt, t3(T)), h2)
66      Empty.absurd({False{} == True{} : Bool}, DM.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(Nat.mul(S, S), Nat.mul(S, S)), False{}, Equal.sym(Bool, Nat.is_lt(Nat.mul(S, S), Nat.mul(S, S)), True{}, h3), N.lt_irrefl(Nat.mul(S, S)))))