def le_ne_succ

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

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

331def le_ne_succ(+a: Nat, +b: Nat, le: {Nat.is_le(a, b) == True{} : Bool}, ne: {Nat.is_eq(a, b) == False{} : Bool}) ->
332  {Nat.is_le(1n+a, b) == True{} : Bool}:
333  match a b:
334    case 0n 0n:
335      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, Arith.clash(Equal.sym(Bool, Nat.is_eq(0n, 0n), False{}, ne)))
336    case 0n 1n+q:
337      Arith.le_zero(q)
338    case 1n+p 0n:
339      Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, Arith.clash(le))
340    case 1n+p 1n+q:
341      le_ne_succ(p, q, le, ne)