GRing.Builders_211val coq_Builders_211_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_HB_unnamed_factory_213 :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isZmodule.axioms_ ->
('a1, 'a1) Zmodule_isComRing.phant_axioms ->
'a1 Zmodule_isRing.axioms_val coq_GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isZmodule.axioms_ ->
('a1, 'a1) Zmodule_isComRing.phant_axioms ->
'a1 Nmodule_isSemiRing.axioms_val coq_Builders_211_R__canonical__GRing_SemiRing :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isZmodule.axioms_ ->
('a1, 'a1) Zmodule_isComRing.phant_axioms ->
SemiRing.coq_typeval coq_HB_unnamed_factory_215 :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isZmodule.axioms_ ->
('a1, 'a1) Zmodule_isComRing.phant_axioms ->
'a1 Ring_hasCommutativeMul.axioms_val coq_GRing_Zmodule_isComRing__to__GRing_SemiRing_hasCommutativeMul :
'a1 Coq_isNmodule.axioms_ ->
'a1 Choice.Coq_hasChoice.axioms_ ->
'a1 Eqtype.Coq_hasDecEq.axioms_ ->
'a1 Nmodule_isZmodule.axioms_ ->
('a1, 'a1) Zmodule_isComRing.phant_axioms ->
'a1 SemiRing_hasCommutativeMul.axioms_