law mul_lt_mul_of_lt_of_lt

bend-mathlib@0.8.1.0 · nat.bend:2904

import bend-mathlib@0.8.1.0/nat.bend as Nat

import Base

2904# Multiplying two strict bounds keeps a strict bound: a < c and b < d imply a * b < c * d.
2905law mul_lt_mul_of_lt_of_lt:
2906  for a: Nat
2907  for b: Nat
2908  for c: Nat
2909  for d: Nat
2910  for h1: lt(a, c)
2911  for h2: lt(b, d)
2912  lt(Nat.mul(a, b), Nat.mul(c, d))

Uses (9)

Used by (2)