def add_zero_left_part

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:399

import Base

399# A product a * b of 0 with a not 0 has b = 0.
400def add_zero_left_part(+b: Nat, +x: Nat, e: {Nat.add(b, x) == 0n : Nat}) -> {b == 0n : Nat}:
401  match b:
402    case 0n:
403      {==}
404    case 1n+q:
405      Empty.absurd({1n+q == 0n : Nat}, nat_clash(Nat.add(q, x), e))