def internal_lt_sub_zero

bend-mathlib@0.8.1.0 · nat.bend:1797

import Base

1797def internal_lt_sub_zero(a: Nat, p: Nat) -> {Nat.is_lt(a, Nat.sub(0n, 1n+p)) == Nat.is_lt(Nat.add(1n+p, a), 0n) : Bool}:
1798  match a:
1799    case 0n:
1800      {==}
1801    case 1n+x:
1802      {==}