law is_lt_eq_succ_le

bend-mathlib@0.8.1.0 · nat.bend:1351

import Base

1351# A < b tests the same as a + 1 <= b.
1352law is_lt_eq_succ_le:
1353  for a: Nat
1354  for b: Nat
1355  {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}