law lt_of_mul_lt_mul_left

bend-mathlib@0.8.1.0 · nat.bend:2876

import Base

2876# A common left factor cancels in a strict inequality: k * a < k * b implies a < b.
2877law lt_of_mul_lt_mul_left:
2878  for k: Nat
2879  for a: Nat
2880  for b: Nat
2881  for h: lt(Nat.mul(k, a), Nat.mul(k, b))
2882  lt(a, b)