law le_max_left

import bend-mathlib@0.8.1.0/nat.bend as Nat

import Base

1160# The left argument is at most the maximum.
1161law le_max_left:
1162  for a: Nat
1163  for b: Nat
1164  le(a, Nat.max(a, b))

Uses (4)