no goals
m n : ℕ
α : Fin (n + 1) → Type u
x✝ : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α (succ i)
i : Fin n
y✝ : α (succ i)
z : α 0
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x₀ y₀ : α 0
x y : (i : Fin n) → α (succ i)
⊢ (∀ (i : Fin n), cons x₀ x (succ i) ≤ cons y₀ y (succ i)) ↔ x ≤ y
simp only [cons_succ, Pi.le_def]