def internal_sub_wrap_arith

bend-mathlib@0.8.1.0 · u32.bend:474

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

474def internal_sub_wrap_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(m, y)) : Nat}:
475  %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(_, y)) : Nat}
476  %MNat.add_sub_cancel_sym(1n+u, y) : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, _) : Nat}
477  %MNat.add_succ_sym(x, u) : {Nat.add(Nat.add(x, u), 1n) == _ : Nat}
478  MNat.add_comm(Nat.add(x, u), 1n)