content: {-# LANGUAGE BangPatterns              #-}
  {-# LANGUAGE EmptyCase                 #-}
  {-# LANGUAGE EmptyDataDecls            #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE OverloadedStrings         #-}
  {-# LANGUAGE PatternSynonyms           #-}
  {-# LANGUAGE RankNTypes                #-}
  {-# LANGUAGE ScopedTypeVariables       #-}
  
  {-# OPTIONS_GHC -Wno-overlapping-patterns #-}
  
  module MAlonzo.Code.Data.Sign.Properties where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Bool qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Algebra.Bundles qualified
  import MAlonzo.Code.Algebra.Structures qualified
  import MAlonzo.Code.Data.Irrelevant qualified
  import MAlonzo.Code.Data.Sign.Base qualified
  import MAlonzo.Code.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
  import MAlonzo.Code.Relation.Binary.Structures qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
  import MAlonzo.Code.Relation.Nullary.Reflects qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Data.Sign.Properties._.IsAbelianGroup
  d_IsAbelianGroup_8 a0 a1 a2 = ()
  -- Data.Sign.Properties._.IsCommutativeMonoid
  d_IsCommutativeMonoid_20 a0 a1 = ()
  -- Data.Sign.Properties._.IsCommutativeSemigroup
  d_IsCommutativeSemigroup_24 a0 = ()
  -- Data.Sign.Properties._.IsGroup
  d_IsGroup_32 a0 a1 a2 = ()
  -- Data.Sign.Properties._.IsMagma
  d_IsMagma_52 a0 = ()
  -- Data.Sign.Properties._.IsMonoid
  d_IsMonoid_58 a0 a1 = ()
  -- Data.Sign.Properties._.IsSemigroup
  d_IsSemigroup_80 a0 = ()
  -- Data.Sign.Properties._.IsAbelianGroup.comm
  d_comm_100 ::
    MAlonzo.Code.Algebra.Structures.T_IsAbelianGroup_1132 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm_100 = erased
  -- Data.Sign.Properties._.IsAbelianGroup.isGroup
  d_isGroup_122 ::
    MAlonzo.Code.Algebra.Structures.T_IsAbelianGroup_1132 ->
    MAlonzo.Code.Algebra.Structures.T_IsGroup_1036
  d_isGroup_122 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isGroup_1144 (coe v0)
  -- Data.Sign.Properties._.IsCommutativeMonoid.comm
  d_comm_390 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm_390 = erased
  -- Data.Sign.Properties._.IsCommutativeMonoid.isMonoid
  d_isMonoid_406 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736 ->
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_isMonoid_406 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v0)
  -- Data.Sign.Properties._.IsCommutativeSemigroup.comm
  d_comm_558 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm_558 = erased
  -- Data.Sign.Properties._.IsCommutativeSemigroup.isSemigroup
  d_isSemigroup_568 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_568 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isSemigroup_556 (coe v0)
  -- Data.Sign.Properties._.IsGroup.inverse
  d_inverse_788 ::
    MAlonzo.Code.Algebra.Structures.T_IsGroup_1036 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inverse_788 v0
    = coe MAlonzo.Code.Algebra.Structures.d_inverse_1052 (coe v0)
  -- Data.Sign.Properties._.IsGroup.isMonoid
  d_isMonoid_802 ::
    MAlonzo.Code.Algebra.Structures.T_IsGroup_1036 ->
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_isMonoid_802 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isMonoid_1050 (coe v0)
  -- Data.Sign.Properties._.IsGroup.⁻¹-cong
  d_'8315''185''45'cong_824 ::
    MAlonzo.Code.Algebra.Structures.T_IsGroup_1036 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8315''185''45'cong_824 = erased
  -- Data.Sign.Properties._.IsMagma.isEquivalence
  d_isEquivalence_1352 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_1352 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v0)
  -- Data.Sign.Properties._.IsMagma.∙-cong
  d_'8729''45'cong_1366 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8729''45'cong_1366 = erased
  -- Data.Sign.Properties._.IsMonoid.identity
  d_identity_1462 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_identity_1462 v0
    = coe MAlonzo.Code.Algebra.Structures.d_identity_698 (coe v0)
  -- Data.Sign.Properties._.IsMonoid.isSemigroup
  d_isSemigroup_1474 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_1474 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v0)
  -- Data.Sign.Properties._.IsSemigroup.assoc
  d_assoc_2206 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc_2206 = erased
  -- Data.Sign.Properties._.IsSemigroup.isMagma
  d_isMagma_2210 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2210 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v0)
  -- Data.Sign.Properties._.Associative
  d_Associative_2544 ::
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_Associative_2544 = erased
  -- Data.Sign.Properties._.Cancellative
  d_Cancellative_2546 ::
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_Cancellative_2546 = erased
  -- Data.Sign.Properties._.Commutative
  d_Commutative_2548 ::
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_Commutative_2548 = erased
  -- Data.Sign.Properties._.Identity
  d_Identity_2564 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_Identity_2564 = erased
  -- Data.Sign.Properties._.Inverse
  d_Inverse_2568 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_Inverse_2568 = erased
  -- Data.Sign.Properties._.Involutive
  d_Involutive_2572 ::
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_Involutive_2572 = erased
  -- Data.Sign.Properties._.LeftCancellative
  d_LeftCancellative_2578 ::
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_LeftCancellative_2578 = erased
  -- Data.Sign.Properties._.LeftIdentity
  d_LeftIdentity_2590 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_LeftIdentity_2590 = erased
  -- Data.Sign.Properties._.RightCancellative
  d_RightCancellative_2608 ::
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_RightCancellative_2608 = erased
  -- Data.Sign.Properties._.RightIdentity
  d_RightIdentity_2620 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_RightIdentity_2620 = erased
  -- Data.Sign.Properties._.SelfInverse
  d_SelfInverse_2632 ::
    (MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
     MAlonzo.Code.Data.Sign.Base.T_Sign_6) ->
    ()
  d_SelfInverse_2632 = erased
  -- Data.Sign.Properties._≟_
  d__'8799'__2650 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d__'8799'__2650 v0 v1
    = case coe v0 of
        MAlonzo.Code.Data.Sign.Base.C_'45'_8
          -> case coe v1 of
               MAlonzo.Code.Data.Sign.Base.C_'45'_8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               MAlonzo.Code.Data.Sign.Base.C_'43'_10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Data.Sign.Base.C_'43'_10
          -> case coe v1 of
               MAlonzo.Code.Data.Sign.Base.C_'45'_8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Data.Sign.Base.C_'43'_10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.Sign.Properties.≡-setoid
  d_'8801''45'setoid_2652 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_'8801''45'setoid_2652
    = coe
        MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402
  -- Data.Sign.Properties.≡-decSetoid
  d_'8801''45'decSetoid_2654 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
  d_'8801''45'decSetoid_2654
    = coe
        MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
        (coe d__'8799'__2650)
  -- Data.Sign.Properties.≡-isDecEquivalence
  d_'8801''45'isDecEquivalence_2656 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
  d_'8801''45'isDecEquivalence_2656
    = coe
        MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isDecEquivalence_398
        (coe d__'8799'__2650)
  -- Data.Sign.Properties.opposite-selfInverse
  d_opposite'45'selfInverse_2658 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_opposite'45'selfInverse_2658 = erased
  -- Data.Sign.Properties.opposite-involutive
  d_opposite'45'involutive_2660 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_opposite'45'involutive_2660 = erased
  -- Data.Sign.Properties.opposite-injective
  d_opposite'45'injective_2662 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_opposite'45'injective_2662 = erased
  -- Data.Sign.Properties.s≢opposite[s]
  d_s'8802'opposite'91's'93'_2666 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_s'8802'opposite'91's'93'_2666 = erased
  -- Data.Sign.Properties.s*s≡+
  d_s'42's'8801''43'_2670 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_s'42's'8801''43'_2670 = erased
  -- Data.Sign.Properties.*-identityˡ
  d_'42''45'identity'737'_2672 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'42''45'identity'737'_2672 = erased
  -- Data.Sign.Properties.*-identityʳ
  d_'42''45'identity'691'_2674 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'42''45'identity'691'_2674 = erased
  -- Data.Sign.Properties.*-identity
  d_'42''45'identity_2676 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'42''45'identity_2676
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Sign.Properties.*-comm
  d_'42''45'comm_2678 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'42''45'comm_2678 = erased
  -- Data.Sign.Properties.*-assoc
  d_'42''45'assoc_2680 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'42''45'assoc_2680 = erased
  -- Data.Sign.Properties.*-cancelʳ-≡
  d_'42''45'cancel'691''45''8801'_2682 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'42''45'cancel'691''45''8801'_2682 = erased
  -- Data.Sign.Properties.*-cancelˡ-≡
  d_'42''45'cancel'737''45''8801'_2688 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'42''45'cancel'737''45''8801'_2688 = erased
  -- Data.Sign.Properties.*-cancel-≡
  d_'42''45'cancel'45''8801'_2694 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'42''45'cancel'45''8801'_2694
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Sign.Properties.*-inverse
  d_'42''45'inverse_2696 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'42''45'inverse_2696
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Sign.Properties.*-isMagma
  d_'42''45'isMagma_2698 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_'42''45'isMagma_2698
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        erased
  -- Data.Sign.Properties.*-magma
  d_'42''45'magma_2700 :: MAlonzo.Code.Algebra.Bundles.T_Magma_68
  d_'42''45'magma_2700
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279
        MAlonzo.Code.Data.Sign.Base.d__'42'__14 d_'42''45'isMagma_2698
  -- Data.Sign.Properties.*-isSemigroup
  d_'42''45'isSemigroup_2702 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_'42''45'isSemigroup_2702
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
        (coe d_'42''45'isMagma_2698) erased
  -- Data.Sign.Properties.*-semigroup
  d_'42''45'semigroup_2704 ::
    MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
  d_'42''45'semigroup_2704
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793
        MAlonzo.Code.Data.Sign.Base.d__'42'__14 d_'42''45'isSemigroup_2702
  -- Data.Sign.Properties.*-isCommutativeSemigroup
  d_'42''45'isCommutativeSemigroup_2706 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemigroup_548
  d_'42''45'isCommutativeSemigroup_2706
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeSemigroup'46'constructor_12093
        (coe d_'42''45'isSemigroup_2702) erased
  -- Data.Sign.Properties.*-commutativeSemigroup
  d_'42''45'commutativeSemigroup_2708 ::
    MAlonzo.Code.Algebra.Bundles.T_CommutativeSemigroup_662
  d_'42''45'commutativeSemigroup_2708
    = coe
        MAlonzo.Code.Algebra.Bundles.C_CommutativeSemigroup'46'constructor_12035
        MAlonzo.Code.Data.Sign.Base.d__'42'__14
        d_'42''45'isCommutativeSemigroup_2706
  -- Data.Sign.Properties.*-isMonoid
  d_'42''45'isMonoid_2710 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_'42''45'isMonoid_2710
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
        (coe d_'42''45'isSemigroup_2702) (coe d_'42''45'identity_2676)
  -- Data.Sign.Properties.*-monoid
  d_'42''45'monoid_2712 :: MAlonzo.Code.Algebra.Bundles.T_Monoid_882
  d_'42''45'monoid_2712
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_16157
        MAlonzo.Code.Data.Sign.Base.d__'42'__14
        (coe MAlonzo.Code.Data.Sign.Base.C_'43'_10) d_'42''45'isMonoid_2710
  -- Data.Sign.Properties.*-isCommutativeMonoid
  d_'42''45'isCommutativeMonoid_2714 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
  d_'42''45'isCommutativeMonoid_2714
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_17695
        (coe d_'42''45'isMonoid_2710) erased
  -- Data.Sign.Properties.*-commutativeMonoid
  d_'42''45'commutativeMonoid_2716 ::
    MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
  d_'42''45'commutativeMonoid_2716
    = coe
        MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_17931
        MAlonzo.Code.Data.Sign.Base.d__'42'__14
        (coe MAlonzo.Code.Data.Sign.Base.C_'43'_10)
        d_'42''45'isCommutativeMonoid_2714
  -- Data.Sign.Properties.*-isGroup
  d_'42''45'isGroup_2718 ::
    MAlonzo.Code.Algebra.Structures.T_IsGroup_1036
  d_'42''45'isGroup_2718
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsGroup'46'constructor_26963
        (coe d_'42''45'isMonoid_2710) (coe d_'42''45'inverse_2696)
        (coe (\ v0 v1 v2 -> v2))
  -- Data.Sign.Properties.*-group
  d_'42''45'group_2720 :: MAlonzo.Code.Algebra.Bundles.T_Group_1520
  d_'42''45'group_2720
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Group'46'constructor_27303
        MAlonzo.Code.Data.Sign.Base.d__'42'__14
        (coe MAlonzo.Code.Data.Sign.Base.C_'43'_10) (\ v0 -> v0)
        d_'42''45'isGroup_2718
  -- Data.Sign.Properties.*-isAbelianGroup
  d_'42''45'isAbelianGroup_2722 ::
    MAlonzo.Code.Algebra.Structures.T_IsAbelianGroup_1132
  d_'42''45'isAbelianGroup_2722
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsAbelianGroup'46'constructor_32441
        (coe d_'42''45'isGroup_2718) erased
  -- Data.Sign.Properties.*-abelianGroup
  d_'42''45'abelianGroup_2724 ::
    MAlonzo.Code.Algebra.Bundles.T_AbelianGroup_1636
  d_'42''45'abelianGroup_2724
    = coe
        MAlonzo.Code.Algebra.Bundles.C_AbelianGroup'46'constructor_29855
        MAlonzo.Code.Data.Sign.Base.d__'42'__14
        (coe MAlonzo.Code.Data.Sign.Base.C_'43'_10) (\ v0 -> v0)
        d_'42''45'isAbelianGroup_2722
  -- Data.Sign.Properties.s*opposite[s]≡-
  d_s'42'opposite'91's'93''8801''45'_2728 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_s'42'opposite'91's'93''8801''45'_2728 = erased
  -- Data.Sign.Properties.opposite[s]*s≡-
  d_opposite'91's'93''42's'8801''45'_2732 ::
    MAlonzo.Code.Data.Sign.Base.T_Sign_6 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_opposite'91's'93''42's'8801''45'_2732 = erased
  