def not_le_add

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:273

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

273def not_le_add(+a: Nat, +b: Nat, +c: Nat, h: {Nat.is_le(a, c) == False{} : Bool}) ->
274  {Nat.is_le(Nat.add(a, b), c) == False{} : Bool}:
275  match a:
276    case 0n:
277      Empty.absurd({Nat.is_le(Nat.add(0n, b), c) == False{} : Bool},
278        Arith.clash_true(Equal.trans(Bool, True{}, Nat.is_le(0n, c), False{},
279          Equal.sym(Bool, Nat.is_le(0n, c), True{}, Arith.le_zero(c)), h)))
280    case 1n+p:
281      match c:
282        case 0n:
283          {==}
284        case 1n+q:
285          not_le_add(p, b, q, h)