law div_mul

lawful-words@0.1.0.0 · proof_nat.bend:1127

import Base

1127law div_mul:
1128  for +a: Nat
1129  for +b: Nat
1130  for +h: {Nat.is_lt(0n, b) == True{} : Bool}
1131  {Nat.div(Nat.mul(a, b), b) == a : Nat}