~/jendhub

def lt_doubled

bendtorch-core@0.1.0.0 · src/storage/arith.bend:314

import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import Base

314def lt_doubled(+x: Nat, +c: Nat, h: {Nat.is_lt(x, Nat.add(c, c)) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(c)) == True{} : Bool}:
315  %double_self(c) : {Nat.is_lt(x, _) == True{} : Bool}
316  h

Uses (6)

Used by (1)