def sub_mono_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:383

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR

383def sub_mono_l(+m: Nat, +n: Nat, +j: Nat, +h: {Nat.is_le(m, n) == True{} : Bool}) -> {Nat.is_le(Nat.sub(m, j), Nat.sub(n, j)) == True{} : Bool}:
384  match m n j:
385    case 0n _ _:
386      L.subst(Nat, z => {Nat.is_le(z, Nat.sub(n, j)) == True{} : Bool}, 0n, Nat.sub(0n, j), Equal.sym(Nat, Nat.sub(0n, j), 0n, NR.zsub(j)), N.zero_le(Nat.sub(n, j)))
387    case 1n+x 0n _:
388      Empty.absurd({Nat.is_le(Nat.sub(1n+x, j), Nat.sub(0n, j)) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
389    case 1n+x 1n+y 0n:
390      h
391    case 1n+ +x 1n+ +y 1n+ +jp:
392      sub_mono_l(x, y, jp, h)