law min_eq_right

bend-mathlib@0.8.1.0 · nat.bend:2387

import Base

2387# The minimum is the smaller argument on the right: b <= a implies min a b = b.
2388law min_eq_right:
2389  for a: Nat
2390  for b: Nat
2391  for h: le(b, a)
2392  {Nat.min(a, b) == b : Nat}