law mul_le_mul

bend-mathlib@0.8.1.0 · nat.bend:2518

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

import Base

2518# Multiplying two bounded factors stays bounded: a <= c and b <= d imply a * b <= c * d.
2519law mul_le_mul:
2520  for a: Nat
2521  for b: Nat
2522  for c: Nat
2523  for d: Nat
2524  for h1: le(a, c)
2525  for h2: le(b, d)
2526  le(Nat.mul(a, b), Nat.mul(c, d))

Uses (6)

Used by (2)