Theorem: List.mem_range2_iff (Logic/Vorspiel/Computability.lean)

State before:
n m i j : ℕ
⊢ (i, j) ∈ range2 n m ↔ i < n ∧ j < m
Tactic:
simp[range2, seq_eq_bind]
State after:
no goals