include "ordered_group.ma".
(*CSC: non capisco questi alias! Una volta non servivano*)
-alias id "plus" = "cic:/matita/groups/plus.con".
+alias id "plus" = "cic:/matita/group/plus.con".
alias symbol "plus" = "Abelian group plus".
record pre_ordered_field_ch0: Type ≝