Ineq.le_mul_r: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as Ineq
Lines 41-45 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&start_line=41&end_line=45

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

# b <= c: a b <= a c
def le_mul_r(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a, b), Nat.mul(a, c)) == True{} : Bool}:
  %Equal.sym(Nat, Nat.mul(a, b), Nat.mul(b, a), NA.mul_comm(a, b)) : {Nat.is_le(_, Nat.mul(a, c)) == True{} : Bool}
  %Equal.sym(Nat, Nat.mul(a, c), Nat.mul(c, a), NA.mul_comm(a, c)) : {Nat.is_le(Nat.mul(b, a), _) == True{} : Bool}
  AR.mul_le(b, c, a, h)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=mul_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm