GRing.Builders_256val coq_Builders_256_R__canonical__GRing_Zmodule :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isZmodule.axioms_ ->
Zmodule.coq_typeval coq_Builders_256_R__canonical__GRing_SemiRing :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isSemiRing.axioms_ ->
SemiRing.coq_typeval coq_HB_unnamed_factory_258 :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isZmodule.axioms_ ->
'a1 Nmodule_isSemiRing.axioms_ ->
'a1 SemiRing_hasCommutativeMul.axioms_ ->
('a1, 'a1, 'a1) ComRing_hasMulInverse.phant_axioms ->
'a1 Ring_hasMulInverse.axioms_