Theorem: Real.neg_log_one_sub_mono (Ray/Dynamics/Multibrot/Log1p.lean)

State before:
x y : ℝ
xy : x ≤ y
y1 : y < 1
⊢ 0 < 1 - y
Tactic:
linarith
State after:
no goals

State before:
x y : ℝ
xy : x ≤ y
y1 : y < 1
⊢ 1 - y ≤ 1 - x
Tactic:
linarith
State after:
no goals