law is_lt_eq_succ_le_sym

bend-mathlib@0.8.1.0 · nat.bend:4274

import Base

4274# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
4275law is_lt_eq_succ_le_sym:
4276  for a: Nat
4277  for b: Nat
4278  {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}