~/jendhub

law le_of_ge

bend-mathlib@0.8.1.0 · nat.bend:538

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

538# Flipping a >= b gives b <= a.
539law le_of_ge:
540  for a: Nat
541  for b: Nat
542  for h: ge(a, b)
543  le(b, a)

Uses (5)

Used by (0)

No other definition uses this definition.