law le_mul_of_pos_left

bend-mathlib@0.8.1.0 · nat.bend:2816

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

import Base

2816# A positive left factor never decreases: m <= (1 + n) * m.
2817law le_mul_of_pos_left:
2818  for m: Nat
2819  for n: Nat
2820  le(m, Nat.mul(1n+n, m))

Uses (4)

Used by (1)

bend-mathlib@0.8.1.0/nat:le_mul_of_pos_right