def internal_sub_arith

bend-mathlib@0.8.1.0 · u32.bend:437

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

437def internal_sub_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, h: MNat.le(y, x), c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(Nat.sub(x, y), m) : Nat}:
438  -d = Nat.sub(x, y)
439  %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(d, _) : Nat}
440  %MNat.add_sub_of_le(y, x, h) : {Nat.add(Nat.add(_, u), 1n) == Nat.add(d, 1n+Nat.add(u, y)) : Nat}
441  -l = Nat.add(Nat.add(Nat.add(y, d), u), 1n)
442  %MNat.add_succ_sym(Nat.sub(x, y), Nat.add(u, y)) : {l == _ : Nat}
443  %MNat.add_comm(1n, Nat.add(Nat.add(y, Nat.sub(x, y)), u)) : {_ == 1n+Nat.add(d, Nat.add(u, y)) : Nat}
444  -l2 = Nat.add(1n, Nat.add(Nat.add(y, d), u))
445  %MNat.add_comm(y, u) : {l2 == 1n+Nat.add(d, _) : Nat}
446  %MNat.add_left_comm(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
447  %MNat.add_assoc(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
448  {==}