def pos_absurd1
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:289
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as Bgcdnat
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/natfuel.bend as NF
289def pos_absurd1(+x: Nat, +hx: {Nat.is_lt(0n, x) == True{} : Bool}, +hb: {Nat.is_lt(x, 1n) == True{} : Bool}) -> Empty:
290 NF.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(0n, x), False{}, Equal.sym(Bool, Nat.is_lt(0n, x), True{}, hx), N.le_not_lt(0n, x, N.lt_succ_le(x, 0n, hb))))