Lemmas about units of ordered rings

theorem Units.index_posSubgroup (R : Type u_1) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] : (posSubgroup R).index = 2