Builders_31 (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Ssralg.GRing.Builders

val coq_Builders_31_R__canonical__eqtype_Equality : 
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  Eqtype.Equality.coq_type

val coq_Builders_31_R__canonical__choice_Choice : 
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  Choice.Choice.coq_type

val coq_Builders_31_R__canonical__GRing_Nmodule : 
  'a1 Coq_isNmodule.axioms_ ->
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  Nmodule.coq_type

val coq_HB_unnamed_factory_33 : 
  'a1 Coq_isNmodule.axioms_ ->
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 Nmodule_isZmodule.axioms_ ->
  ('a1, 'a1) Zmodule_isRing.phant_axioms ->
  'a1 Nmodule_isSemiRing.axioms_