law min_eq_left

bend-mathlib@0.8.1.0 · nat.bend:2370

import Base

2370# The minimum is the smaller argument on the left: a <= b implies min a b = a.
2371law min_eq_left:
2372  for a: Nat
2373  for b: Nat
2374  for h: le(a, b)
2375  {Nat.min(a, b) == a : Nat}