law lt_iff_le_and_ne_sym

bend-mathlib@0.8.1.0 · nat.bend:4599

import Base

4599# Below means at most and different: a < b tests as a <= b and not a = b, reversed to rewrite toward the simple side.
4600law lt_iff_le_and_ne_sym:
4601  for a: Nat
4602  for b: Nat
4603  {Bool.and(Nat.is_le(a, b), Bool.not(Nat.is_eq(a, b))) == Nat.is_lt(a, b) : Bool}