~/jendhub

law lt_of_gt

bend-mathlib@0.8.1.0 · nat.bend:574

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

574# Flipping a > b gives b < a.
575law lt_of_gt:
576  for a: Nat
577  for b: Nat
578  for h: gt(a, b)
579  lt(b, a)

Uses (5)

Used by (0)

No other definition uses this definition.