law mod_eq_of_lt

bend-mathlib@0.8.1.0 · nat.bend:2002

import Base

2002# A number below the divisor is its own remainder: a < b implies a % b = a.
2003law mod_eq_of_lt:
2004  for a: Nat
2005  for b: Nat
2006  for h: lt(a, b)
2007  {Nat.mod(a, b) == a : Nat}