law nat_div_lt

lawful-words@0.1.0.0 · LAWS.bend:554

import Base

554# a < b * c with b > 0 gives a / b < c.
555law nat_div_lt:
556  for a: Nat
557  for b: Nat
558  for c: Nat
559  for hb: {Nat.is_lt(0n, b) == True{} : Bool}
560  for h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool}
561  {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}