law mul_lt_mul_of_pos_right

bend-mathlib@0.8.1.0 · nat.bend:2853

import Base

2853# Multiplying on the right by a positive factor preserves the strict order: a < b implies a * (1 + k) < b * (1 + k).
2854law mul_lt_mul_of_pos_right:
2855  for a: Nat
2856  for b: Nat
2857  for k: Nat
2858  for h: lt(a, b)
2859  lt(Nat.mul(a, 1n+k), Nat.mul(b, 1n+k))