for G being addGroup
for H being strict Subgroup of G st Left_Cosets H is finite & Index H = card G holds
( G is finite & H = (0). G )