~/jendhub

law ge_of_le

bend-mathlib@0.8.1.0 · nat.bend:556

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

556# Flipping b <= a gives a >= b.
557law ge_of_le:
558  for a: Nat
559  for b: Nat
560  for h: le(b, a)
561  ge(a, b)

Uses (5)

Used by (0)

No other definition uses this definition.