for G being addGroup
for H being Subgroup of G holds Left_Cosets H, Right_Cosets H are_equipotent