def half_le

bend-collections-laws-math@1.0.0.0 · proofs/lib/two_list.bend:47

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

47# half of a nonempty length is below it
48def half_le(+n: Nat) -> {Nat.is_le(Nat.div(1n+n, 2n), n) == True{} : Bool}:
49  match n:
50    case 0n:
51      {==}
52    case 1n+0n:
53      {==}
54    case 1n+1n+k:
55      %Equal.sym(Nat, Nat.div(Nat.add(2n, 1n+k), 2n), 1n+Nat.div(1n+k, 2n), N.div2_step(1n+k)) : {Nat.is_le(_, 2n+k) == True{} : Bool}
56      N.le_trans(1n+Nat.div(1n+k, 2n), 1n+k, 2n+k, half_le(k), N.le_succ(1n+k))