def half_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:737

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

737def half_le(+n: Nat) -> {Nat.is_le(C.half(n), n) == True{} : Bool}:
738  match n:
739    case 0n:
740      {==}
741    case 1n:
742      {==}
743    case 2n+ +p:
744      N.le_trans(1n+C.half(p), 1n+p, 2n+p, half_le(p), N.le_succ(1n+p))