law is_gt_eq_is_lt

bend-mathlib@0.8.1.0 · nat.bend:1333

import Base

1333# A > b tests the same as b < a.
1334law is_gt_eq_is_lt:
1335  for a: Nat
1336  for b: Nat
1337  {Nat.is_gt(a, b) == Nat.is_lt(b, a) : Bool}