(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/ordered_fields_ch0/".
+
include "attic/fields.ma".
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 ≝
]
qed.
-coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con.
+coercion cic:/matita/attic/ordered_fields_ch0/of_ordered_abelian_group.con.
(*CSC: I am not able to prove this since unfold is undone by coercion composition*)
axiom of_with1:
]
qed.
-coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
+coercion cic:/matita/attic/ordered_fields_ch0/of_cotransitively_ordered_set.con.
record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
{ of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;