law le_antisymm

bend-mathlib@0.8.1.0 · nat.bend:430

import Base

430# The order is antisymmetric: a <= b and b <= a imply a = b.
431law le_antisymm:
432  for a: Nat
433  for b: Nat
434  for ab: le(a, b)
435  for ba: le(b, a)
436  {a == b : Nat}