def le_mul_pos

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/ineq.bend:82

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

82# a <= a + b, and a <= a * b for b >= 1
83def le_mul_pos(+a: Nat, +b: Nat, +h: {Nat.is_le(1n, b) == True{} : Bool}) -> {Nat.is_le(a, Nat.mul(a, b)) == True{} : Bool}:
84  le_subst_l(Nat.mul(a, 1n), a, Nat.mul(a, b), NA.mul_one(a), le_mul_r(a, 1n, b, h))