~/jendhub

law mul_self_lt_mul_self

bend-mathlib@0.8.1.0 · nat.bend:2937

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

2937# Squares are strictly monotone: a < b implies a * a < b * b.
2938law mul_self_lt_mul_self:
2939  for a: Nat
2940  for b: Nat
2941  for h: lt(a, b)
2942  lt(Nat.mul(a, a), Nat.mul(b, b))

Uses (4)

Used by (0)

No other definition uses this definition.