law div_lt

lawful-words@0.1.0.0 · proof_nat.bend:1361

import Base

1361law div_lt:
1362  for +a: Nat
1363  for +b: Nat
1364  for +c: Nat
1365  for +hb: {Nat.is_lt(0n, b) == True{} : Bool}
1366  for +h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool}
1367  {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}