def below_one_more

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:67

import Base

67def below_one_more(+rest: Nat) -> {Nat.is_lt(1n+rest, 0n) == Nat.is_lt(1n+rest, 1n) : Bool}:
68  match rest:
69    case 0n:
70      {==}
71    case 1n+deeper:
72      {==}