def mul_lt_cancel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/reduce.bend:74

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR

74# T a < T b gives a < b
75def mul_lt_cancel(+t: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(Nat.mul(a, t), Nat.mul(b, t)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
76  match c:
77    case True{}:
78      hc
79    case False{}:
80      +le = AR.mul_le(b, a, t, N.not_lt_le(a, b, hc))
81      Empty.absurd({Nat.is_lt(a, b) == True{} : Bool}, Lg.true_not_false(Nat.is_lt(Nat.mul(a, t), Nat.mul(b, t)), h, N.le_not_lt(Nat.mul(a, t), Nat.mul(b, t), le)))