~/jendhub

def succ_add_ne

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

import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
import Base

30def succ_add_ne(+left: Nat, +right: Nat) -> {False{} == Nat.is_eq(1n+Nat.add(left, right), right) : Bool}:
31  match right:
32    case 0n:
33      {==}
34    case 1n+rest:
35      %Equal.sym(Nat, Nat.add(left, 1n+rest), 1n+Nat.add(left, rest), add_succ(left, rest)) :
36        {False{} == Nat.is_eq(1n+_, 1n+rest) : Bool}
37      succ_add_ne(left, rest)

Uses (6)

Used by (1)