Module POrderedZmodule.Exports

val coq_Num_POrderedZmodule_class__to__Order_POrder_class : 'a1 axioms_ -> 'a1 Order.Order.POrder.axioms_
val coq_Num_POrderedZmodule__to__Order_POrder : coq_type -> Order.Order.POrder.coq_type
val coq_Num_POrderedZmodule_class__to__GRing_Nmodule_class : 'a1 axioms_ -> 'a1 Ssralg.GRing.Nmodule.axioms_
val coq_Num_POrderedZmodule__to__GRing_Nmodule : coq_type -> Ssralg.GRing.Nmodule.coq_type
val join_Num_POrderedZmodule_between_GRing_Nmodule_and_Order_POrder : coq_type -> Order.Order.POrder.coq_type