α : Type u
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (Chain r 0 (map succ (range n)) ↔ Chain' (fun m => r m) (0 :: map succ (range n)))
α : Type u
r : ℕ → ℕ → Prop
n a : ℕ
⊢ Chain r a (range (succ n)) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m (succ m)
rw [range_succ_eq_map, chain_cons, and_congr_right_iff, ← chain'_range_succ, range_succ_eq_map]
no goals
α : Type u
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (Chain r 0 (map succ (range n)) ↔ Chain' (fun m => r m) (0 :: map succ (range n)))
exact fun _ => Iff.rfl