Disjoint halves of a finite index set

The two inclusions of an index into the doubled finite set have distinct values.

theorem RS.castAdd_ne_natAdd {n : ℕ} (i : Fin n) : Fin.castAdd n i ≠ Fin.natAdd n i

The two inclusions of the same finite index have distinct values.