~/jendhub

def le_mul2

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

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as Ineq
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/arith.bend as AR

47# a <= c, b <= d: a b <= c d
48def le_mul2(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +h1: {Nat.is_le(a, c) == True{} : Bool}, +h2: {Nat.is_le(b, d) == True{} : Bool}) -> {Nat.is_le(Nat.mul(a, b), Nat.mul(c, d)) == True{} : Bool}:
49  N.le_trans(Nat.mul(a, b), Nat.mul(c, b), Nat.mul(c, d), AR.mul_le(a, c, b, h1), le_mul_r(c, b, d, h2))

Uses (7)

Used by (4)