Library HoTT.Tests.Algebra.Groups.Group

From HoTT Require Import Basics.Overture Algebra.Groups.Group.

Test that opposite groups are definitionally involutive.
Succeed Definition test1 (G : Group) : G = (grp_op (grp_op G)) :> Group := 1.