Proving cancellation of deriv at non-differentiable points

Stream: Is there code for X?

[Ryan Lahfa]

I am still going through the derivatives API and if I understand well, deriv will return 0 if it's non-differentiable at this point.
Proving this requires to prove non-differentiability, but I am under the impression that either I am missing some functions or tricks or there might be some API missing.

Namely, I would have tried to use notdiff to prove that $\log \circ (x + 1)$ is non-differentiable at $-1$ by proving that $\log \circ (x + 1) \circ (x - 1)$ is not at $0$ and $x - 1$ is differentiable at $1$, but it is getting messy and convert do not want to let me show that $\log \circ (x + 1) \circ (x - 1) = \log$ or things like that.

Obligatory MWE (I can rewrite to remove the add_comm thing which is useless in this context):

import analysis.calculus.deriv
import analysis.special_functions.exp_log

lemma deriv.log_1_plus_x: deriv (λ (x: ℝ), real.log (1 + x)) = λ (x: ℝ), if x = -1 then 0 else (1 / (1 + x)) :=
begin
  ext,
  by_cases (x = -1),
  {
    rw [if_pos h],
    have := (mt real.differentiable_at_log_iff.1) (not_not.2 ((add_eq_zero_iff_eq_neg.2) h)),
    rw [add_comm _ _] at this,
    apply deriv_zero_of_not_differentiable_at,
    -- have notdiff := (mt (differentiable_at.comp x)),
    -- rw [not_imp] at notdiff,
    sorry,
  },
  {
    rw [if_neg h],
    convert deriv.log _ _,
    repeat { simp [add_comm 1 x, (mt add_eq_zero_iff_eq_neg.1) h] },
  },
end