~/jendhub

law mul_self_le_mul_self

bend-mathlib@0.8.1.0 · nat.bend:2924

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

2924# Squares are monotone: a <= b implies a * a <= b * b.
2925law mul_self_le_mul_self:
2926  for a: Nat
2927  for b: Nat
2928  for h: le(a, b)
2929  le(Nat.mul(a, a), Nat.mul(b, b))

Uses (4)

Used by (0)

No other definition uses this definition.