def dle

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

import Base

495# 2 q <= 2 p gives q <= p
496def dle(+q: Nat, +p: Nat, +h: {Nat.is_le(Nat.double(q), Nat.double(p)) == True{} : Bool}) -> {Nat.is_le(q, p) == True{} : Bool}:
497  dle_c(q, p, h, Nat.is_lt(p, q), {==})