simp [Membership.mem, contains]
x : ℕ
r : Range
⊢ x ∈ r ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start
x : ℕ
r : Range
⊢ (r.start ≤ x ∧ x < r.stop) ∧ r.step ∣ x - r.start ↔ r.start ≤ x ∧ x < r.stop ∧ r.step ∣ x - r.start