PUnit.commGroup =
  { mul := fun x x_1 => PUnit.unit, mul_assoc := PUnit.commGroup._proof_5, one := PUnit.unit,
    one_mul := PUnit.commGroup._proof_6, mul_one := PUnit.commGroup._proof_7, npow_zero := PUnit.commGroup._proof_1,
    npow_succ := PUnit.commGroup._proof_2, inv := fun x => PUnit.unit, div_eq_mul_inv := PUnit.commGroup._proof_3,
    zpow_zero' := PUnit.commGroup._proof_1, zpow_succ' := PUnit.commGroup._proof_2,
    zpow_neg' := PUnit.commGroup._proof_4, inv_mul_cancel := PUnit.commGroup._proof_8,
    mul_comm := PUnit.commGroup._proof_9 }