@[reducible, inline]

abbrev Nat.avg (a b : Nat) : Nat

Average of two natural numbers rounded toward zero.

theorem Nat.avg_comm (a b : Nat) : a.avg b = b.avg a

theorem Nat.avg_le_left {b a : Nat} (h : b ≤ a) : a.avg b ≤ a

theorem Nat.avg_le_right {a b : Nat} (h : a ≤ b) : a.avg b ≤ b

theorem Nat.avg_lt_left {b a : Nat} (h : b < a) : a.avg b < a

theorem Nat.avg_lt_right {a b : Nat} (h : a < b) : a.avg b < b

theorem Nat.le_avg_left {a b : Nat} (h : a ≤ b) : a ≤ a.avg b

theorem Nat.le_avg_right {b a : Nat} (h : b ≤ a) : b ≤ a.avg b

theorem Nat.le_add_one_of_avg_eq_left {a b : Nat} (h : a.avg b = a) : b ≤ a + 1

theorem Nat.le_add_one_of_avg_eq_right {a b : Nat} (h : a.avg b = b) : a ≤ b + 1

@[irreducible]

def Nat.bisect {start stop : Nat} {p : Nat → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false) : Nat

Given natural numbers a < b such that p a = true and p b = false, bisect finds a natural number a ≤ c < b such that p c = true and p (c+1) = false.

@[irreducible]

theorem Nat.bisect_lt_stop {start stop : Nat} {p : Nat → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false) : bisect h hstart hstop < stop

@[irreducible]

theorem Nat.start_le_bisect {start stop : Nat} {p : Nat → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false) : start ≤ bisect h hstart hstop

@[irreducible]

theorem Nat.bisect_true {start stop : Nat} {p : Nat → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false) : p (bisect h hstart hstop) = true

@[irreducible]

theorem Nat.bisect_add_one_false {start stop : Nat} {p : Nat → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false) : p (bisect h hstart hstop + 1) = false