law n_mod_small

lawful-arrays@0.1.0.0 · proof_words.bend:71

import Base

71law n_mod_small:
72  for +a: Nat
73  for +b: Nat
74  for +h: {Nat.is_lt(a, b) == True{} : Bool}
75  {Nat.mod(a, b) == a : Nat}