~/jendhub

def wsh.m0

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:393

import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

393# 10 x + y = 0: x = 0
394def wsh.m0(x: Nat, +y: Nat, e: {Nat.add(Nat.mul(x, 10n), y) == 0n : Nat}) -> {x == 0n : Nat}:
395  match x:
396    case 0n:
397      {==}
398    case 1n+ +p:
399      Empty.absurd({1n+p == 0n : Nat}, UL.nat_succ_add_absurd(Nat.add(Nat.add(9n, Nat.mul(p, 10n)), y), 0n, Equal.trans(Nat, Nat.add(Nat.add(Nat.add(9n, Nat.mul(p, 10n)), y), 1n), Nat.add(Nat.mul(1n+p, 10n), y), 0n, wr.t10(p, y), e)))

Uses (7)

Used by (1)