law is_gt_eq_is_lt_sym

bend-mathlib@0.8.1.0 · nat.bend:4265

import Base

4265# A > b tests the same as b < a, reversed to rewrite toward the simple side.
4266law is_gt_eq_is_lt_sym:
4267  for a: Nat
4268  for b: Nat
4269  {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}