Stable Fin (n + 1) head index

Compared Scott permutation/cancellation conditions mention the distinguished index 0 : Fin (n + 1). Elaborating that literal attaches a generated ._proof_N to whichever declaration first needs OfNat. Palomar compares those generated constants, so Challenge and Solution must share a named proof of 0 < n + 1 instead.

theorem Scott1964.MeasurementStructures.fin_succ_pos (n : ℕ) : 0 < n + 1

def Scott1964.MeasurementStructures.finHead (n : ℕ) : Fin (n + 1)

The distinguished index in a nonempty Scott sequence of length n + 1.

Equations

• Scott1964.MeasurementStructures.finHead n = ⟨0, ⋯⟩

theorem Scott1964.MeasurementStructures.finHead_eq_zero (n : ℕ) : finHead n = 0