law hdm

lawful-fields@0.1.1.0 · proof_digits.bend:497

import Base

497law hdm:
498  for +m: Nat
499  {Nat.is_le(Nat.div(m, 10n), m) == True{} : Bool}