F64bl.dle: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as F64bl
Lines 76-77 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend&start_line=76&end_line=77

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

def dle(+a: Nat, +c: Nat, +h: {Nat.is_le(Nat.double(a), Nat.double(c)) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
  Equal.trans(Bool, Nat.is_le(a, c), Nat.is_le(Nat.double(a), Nat.double(c)), True{}, Equal.cong(Cmp, Bool, t => Cmp.is_le(t), Nat.cmp(a, c), Nat.cmp(Nat.double(a), Nat.double(c)), Equal.sym(Cmp, Nat.cmp(Nat.double(a), Nat.double(c)), Nat.cmp(a, c), NC.cmp_dbl(a, c))), h)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=cmp_dbl