def neither_below

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:513

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

513def neither_below(+left: Nat, +right: Nat, first: {Nat.is_lt(left, right) == False{} : Bool},
514  second: {Nat.is_lt(right, left) == False{} : Bool}) -> {left == right : Nat}:
515  match left right:
516    case 0n 0n:
517      {==}
518    case 0n 1n+r:
519      Empty.absurd({0n == 1n+r : Nat}, Arith.clash_true(first))
520    case 1n+l 0n:
521      Empty.absurd({1n+l == 0n : Nat}, Arith.clash_true(second))
522    case 1n+l 1n+r:
523      Equal.cong(Nat, Nat, n => 1n+n, l, r, neither_below(l, r, first, second))