law is_ge_eq_is_le_sym

bend-mathlib@0.8.1.0 · nat.bend:4256

import Base

4256# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
4257law is_ge_eq_is_le_sym:
4258  for a: Nat
4259  for b: Nat
4260  {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}