def not_lt_succ_lt

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

import Base

68def not_lt_succ_lt(+id: Nat, +bound: Nat, outside: {Nat.is_lt(id, 1n+bound) == False{} : Bool}) ->
69  {Nat.is_lt(id, bound) == False{} : Bool}:
70  match id bound:
71    case 0n bound:
72      Empty.absurd({Nat.is_lt(0n, bound) == False{} : Bool}, true_false(outside))
73    case 1n+rest 0n:
74      {==}
75    case 1n+rest 1n+smaller:
76      not_lt_succ_lt(rest, smaller, outside)