def not_lt_succ_ne

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:58

import Base

58def not_lt_succ_ne(+id: Nat, +bound: Nat, outside: {Nat.is_lt(id, 1n+bound) == False{} : Bool}) ->
59  {False{} == Nat.is_eq(bound, id) : Bool}:
60  match id bound:
61    case 0n bound:
62      Empty.absurd({False{} == Nat.is_eq(bound, 0n) : Bool}, true_false(outside))
63    case 1n+rest 0n:
64      {==}
65    case 1n+rest 1n+smaller:
66      not_lt_succ_ne(rest, smaller, outside)