law lt_of_mul_lt_mul_right

bend-mathlib@0.8.1.0 · nat.bend:2890

import Base

2890# A common right factor cancels in a strict inequality: a * k < b * k implies a < b.
2891law lt_of_mul_lt_mul_right:
2892  for a: Nat
2893  for b: Nat
2894  for k: Nat
2895  for h: lt(Nat.mul(a, k), Nat.mul(b, k))
2896  lt(a, b)