law div_le_div

bend-mathlib@0.8.1.0 · nat.bend:856

import Base

856# Division by a positive divisor is monotone: a <= c implies a / (1 + b) <= c / (1 + b).
857law div_le_div:
858  for +a: Nat
859  for +c: Nat
860  for b: Nat
861  for h: le(a, c)
862  le(Nat.div(a, 1n+b), Nat.div(c, 1n+b))