def shl_inv_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64mont.bend:44

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/width.bend as WW

44# shift(k, a) < shift(k, b) gives a < b
45def shl_inv_c(+k: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {c == True{} : Bool}:
46  match c:
47    case True{}:
48      {==}
49    case False{}:
50      +h2 = WW.shift_mono(k, b, a, N.not_lt_le(a, b, hc))
51      Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(C.shift(k, a), C.shift(k, b)), False{}, Equal.sym(Bool, Nat.is_lt(C.shift(k, a), C.shift(k, b)), True{}, h), N.le_not_lt(C.shift(k, a), C.shift(k, b), h2))))