~/jendhub

def internal_div_zero_of_wit

bend-mathlib@0.8.1.0 · nat.bend:807

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

807def internal_div_zero_of_wit(+a: Nat, +b: Nat, w: &k:Nat -> {Nat.add(a, k) == b : Nat}) -> {Nat.div(a, 1n+b) == 0n : Nat}:
808  match w:
809    case (+k, e):
810      %e : {Nat.div(a, 1n+_) == 0n : Nat}
811      Equal.sym(Nat, 0n, Pair.fst(Nat, Nat, Nat.divmod.go(a, Nat.add(a, k), 0n, 0n)), internal_div_go_small(a, k, 0n, 0n))

Uses (9)

Used by (1)