Misc prereqs and collect imports

theorem Fin.ne_zero_iff_eq_one {x : Fin 2} : x ≠ 0 ↔ x = 1

theorem Fin.eq_zero_iff_ne_one {x : Fin 2} : x = 0 ↔ x ≠ 1

theorem Fin.fin_two_eq_zero_of_ne_one {x : Fin 2} (hx : x ≠ 1) : x = 0