def earlier_zero_false
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:260
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
import Base
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
260def earlier_zero_false(+other: Nat, earlier: {Nat.is_lt(other, 0n) == True{} : Bool}) -> Empty:
261 Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_lt(other, 0n), False{},
262 Equal.sym(Bool, Nat.is_lt(other, 0n), True{}, earlier), lt_zero_false(other)))