law lt_mul_r

lawful-words@0.1.0.0 · proof_bytes.bend:1412

import Base

1412law lt_mul_r:
1413  for +a: Nat
1414  for +b: Nat
1415  for +c: Nat
1416  for +h: {Nat.is_lt(a, b) == True{} : Bool}
1417  for +hc: {Nat.is_lt(0n, c) == True{} : Bool}
1418  {Nat.is_lt(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}