Split ne into lt, gt cases

Stream: new members

[Icaro Costa]

How do I split $r\neq$ into two cases $r > 1$ and $r < 1$?

example {a r : ℝ} (n : ℕ) (h : r ≠ 1) : ∑ i ∈ range (n+1), a * r^i = (a * r^(n+1) - a) / (r-1) := by
cases le_or_gt_of_ne h

[Notification Bot]

A message was moved here from #new members > Variable Macro For bv_decide by Ruben Van de Velde.

[Ruben Van de Velde]

Please share a #mwe