law nat_mul_lt

bend-osdev-u32@0.1.0.0 · LAWS.bend:670

import Base

670law nat_mul_lt:
671  for +a: Nat
672  for +b: Nat
673  for +c: Nat
674  for +d: Nat
675  for h1: {Nat.is_lt(a, c) == True{} : Bool}
676  for h2: {Nat.is_lt(b, d) == True{} : Bool}
677  {Nat.is_lt(Nat.mul(a, b), Nat.mul(c, d)) == True{} : Bool}