F64sqc.halve: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc
Lines 62-63 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend&start_line=62&end_line=63

import Base

def halve(+x: Nat, +y: Nat, +h: {Nat.is_le(Nat.add(x, x), Nat.add(y, y)) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
  halve_c(x, y, h, Nat.is_le(x, y), {==})

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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/f64sqc.bend&name=halve_c