law mul_lt_mul_of_pos_left

bend-mathlib@0.8.1.0 · nat.bend:2838

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

import Base

2838# Multiplying on the left by a positive factor preserves the strict order: a < b implies (1 + k) * a < (1 + k) * b.
2839law mul_lt_mul_of_pos_left:
2840  for a: Nat
2841  for b: Nat
2842  for k: Nat
2843  for h: lt(a, b)
2844  lt(Nat.mul(1n+k, a), Nat.mul(1n+k, b))

Uses (9)

Used by (3)