law le_mul_l

lawful-words@0.1.0.0 · proof_nat.bend:911

import Base

911law le_mul_l:
912  for +c: Nat
913  for +a: Nat
914  for +b: Nat
915  for e: {Nat.is_le(a, b) == True{} : Bool}
916  {Nat.is_le(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool}