no goals
α : Type ?u.317005
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range (Nat.succ n)) ↔ r n 0 ∧ ∀ (m : ℕ), m < n → r m (Nat.succ m)
rw [range_succ, ← coe_cons_eq_coe_append, chain_coe_cons, ← range_succ, chain_range_succ]