Normalized heights in the unit interval

The normalized height (r - a) / (b - a) of a point r ∈ [a, b] lies in the unit interval, including in the degenerate case a = b, where Lean's convention x / 0 = 0 makes it 0.

theorem TauCeti.sub_div_sub_mem_unitInterval {a b r : ℝ} (har : a ≤ r) (hrb : r ≤ b) : (r - a) / (b - a) ∈ unitInterval

The normalized height of r ∈ [a, b] lies in [0, 1], also when a = b.