Zulip Chat Archive
Stream: new members
Topic: Stuck at a trivial list property
Martin Dvořák (Feb 07 2022 at 08:05):
Can you please help me with proving the following trivial list property?
import tactic
example (a b : list ℕ) : (a ++ 42 :: b).nth a.length = ↑42 :=
sorry
Last updated: May 02 2025 at 03:31 UTC