m s n : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n
m s n : Nat
⊢ m ∈ range' s n ↔ s ≤ m ∧ m < s + n
simp [mem_range']
no goals
m s n : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n
exact ⟨
fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩