law div_mono10

lawful-fields@0.1.1.0 · proof_digits.bend:509

import Base

509law div_mono10:
510  for +a: Nat
511  for +b: Nat
512  for +h: {Nat.is_le(a, b) == True{} : Bool}
513  {Nat.is_le(Nat.div(a, 10n), Nat.div(b, 10n)) == True{} : Bool}