begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
:: deftheorem defines Double_Cosets GROUP_8:def 1 :
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem