law lt_iff_le_and_ne

bend-mathlib@0.8.1.0 · nat.bend:2640

import Base

2640# Below means at most and different: a < b tests as a <= b and not a = b.
2641law lt_iff_le_and_ne:
2642  for a: Nat
2643  for b: Nat
2644  {Nat.is_lt(a, b) == Bool.and(Nat.is_le(a, b), Bool.not(Nat.is_eq(a, b))) : Bool}