law le_zero_eq

bend-mathlib@0.8.1.0 · nat.bend:1559

import Base

1559# The only natural at most zero is zero.
1560law le_zero_eq:
1561  for n: Nat
1562  for h: le(n, 0n)
1563  {n == 0n : Nat}