law lt_mul_cancel

lawful-words@0.1.0.0 · proof_nat.bend:1564

import Base

1564law lt_mul_cancel:
1565  for +c: Nat
1566  for +a: Nat
1567  for +b: Nat
1568  for +h: {Nat.is_lt(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool}
1569  {Nat.is_lt(a, b) == True{} : Bool}