~/jendhub

law gt_of_lt

bend-mathlib@0.8.1.0 · nat.bend:592

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

592# Flipping b < a gives a > b.
593law gt_of_lt:
594  for a: Nat
595  for b: Nat
596  for h: lt(b, a)
597  gt(a, b)

Uses (5)

Used by (0)

No other definition uses this definition.