no goals
b x y : Ordinal
xy : x ≤ y
hx : x = 0
⊢ log b x ≤ log b y
simp only [hx, log_zero_right, Ordinal.zero_le]
no goals
b x y : Ordinal
xy : x ≤ y
hx : ¬x = 0
hb : ¬1 < b
⊢ log b x ≤ log b y
simp only [log_of_not_one_lt_left hb, Ordinal.zero_le]