law le_mul_r

lawful-words@0.1.0.0 · proof_nat.bend:894

import Base

894# a <= b gives a * c <= b * c.
895law le_mul_r:
896  for +a: Nat
897  for +b: Nat
898  for +c: Nat
899  for e: {Nat.is_le(a, b) == True{} : Bool}
900  {Nat.is_le(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}