law is_ge_eq_is_le

bend-mathlib@0.8.1.0 · nat.bend:1315

import Base

1315# A >= b tests the same as b <= a.
1316law is_ge_eq_is_le:
1317  for a: Nat
1318  for b: Nat
1319  {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}