law min_le_left

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

import Base

1126# The minimum is at most its left argument.
1127law min_le_left:
1128  for a: Nat
1129  for b: Nat
1130  le(Nat.min(a, b), a)

Uses (3)