law le_mul_pos

lawful-words@0.1.0.0 · proof_bytes.bend:1466

import Base

1466law le_mul_pos:
1467  for +x: Nat
1468  for +c: Nat
1469  for +hc: {Nat.is_lt(0n, c) == True{} : Bool}
1470  {Nat.is_le(x, Nat.mul(x, c)) == True{} : Bool}