def lt_sub_pos

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:814

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/math/typed/natcmp.bend as NC

814def lt_sub_pos(+x: Nat, +n: Nat, +h: {Nat.is_lt(x, n) == True{} : Bool}) -> {Nat.is_le(1n, Nat.sub(n, x)) == True{} : Bool}:
815  match x n:
816    case 0n 0n:
817      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, h)
818    case 0n 1n+ +np:
819      N.zero_le(np)
820    case 1n+ +xp 0n:
821      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, h)
822    case 1n+ +xp 1n+ +np:
823      lt_sub_pos(xp, np, h)