def lt_succ_eq

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:26

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

26def lt_succ_eq(+r: Nat, +size: Nat, below: {Nat.is_lt(r, size) == True{} : Bool},
27  not_below: {False{} == Nat.is_lt(1n+r, size) : Bool}) -> {size == 1n+r : Nat}:
28  match r size:
29    case 0n 0n:
30      Empty.absurd({0n == 1n : Nat}, Arith.clash(below))
31    case 0n 1n+s:
32      match s:
33        case 0n:
34          {==}
35        case 1n+t:
36          Empty.absurd({2n+t == 1n : Nat}, Arith.clash(not_below))
37    case 1n+p 0n:
38      Empty.absurd({0n == 2n+p : Nat}, Arith.clash(below))
39    case 1n+p 1n+s:
40      Equal.cong(Nat, Nat, n => 1n+n, s, 1n+p, lt_succ_eq(p, s, below, not_below))