~/jendhub

law le_mul_of_pos_right

bend-mathlib@0.8.1.0 · nat.bend:2826

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

2826# A positive right factor never decreases: m <= m * (1 + n).
2827law le_mul_of_pos_right:
2828  for m: Nat
2829  for n: Nat
2830  le(m, Nat.mul(m, 1n+n))

Uses (5)

Used by (0)

No other definition uses this definition.