law div_eq_zero_of_le

bend-mathlib@0.8.1.0 · nat.bend:813

import Base

813# A number at most b divides by 1 + b to zero: a <= b implies a / (1 + b) = 0.
814law div_eq_zero_of_le:
815  for +a: Nat
816  for +b: Nat
817  for h: le(a, b)
818  {Nat.div(a, 1n+b) == 0n : Nat}