-record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Prop \def
- { of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
- of_plus_compat: ∀a,b,c. le a b → le (a+c) (b+c);
- of_weak_tricotomy : ∀a,b. a≠b → le a b ∨ le b a;
+(*CSC: non capisco questi alias! Una volta non servivano*)
+alias id "plus" = "cic:/matita/groups/plus.con".
+alias symbol "plus" = "Abelian group plus".
+
+record pre_ordered_field_ch0: Type ≝
+ { of_field:> field;
+ of_cotransitively_ordered_set_: cotransitively_ordered_set;
+ of_with: os_carrier of_cotransitively_ordered_set_ = carrier of_field
+ }.
+
+(*CSC: the following lemma (that is also a coercion) should be automatically
+ generated *)
+lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set.
+ intro F;
+ apply mk_cotransitively_ordered_set;
+ [ apply mk_ordered_set;
+ [ apply (carrier F)
+ | apply
+ (eq_rect ? ? (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) ? (of_with F))
+ | apply
+ (eq_rect' Type (os_carrier (of_cotransitively_ordered_set_ F))
+ (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
+ is_order_relation a (eq_rect Type (os_carrier (of_cotransitively_ordered_set_ F)) (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) a H))
+ ? (Type_OF_pre_ordered_field_ch0 F) (of_with F));
+ simplify;
+ apply (os_order_relation_properties (of_cotransitively_ordered_set_ F))
+ ]
+ | simplify;
+ apply
+ (eq_rect' ? ?
+ (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
+ cotransitive a
+ match H in eq
+ return
+ λa2:Type.λH1:os_carrier (of_cotransitively_ordered_set_ F)=a2.
+ a2→a2→Prop
+ with
+ [refl_eq ⇒ os_le (of_cotransitively_ordered_set_ F)])
+ ? ? (of_with F));
+ simplify;
+ apply cos_cotransitive
+ ].
+qed.
+
+coercion cic:/matita/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;
+ of_plus_compat: ∀a,b,c:F. a≤b → a+c≤b+c;
+ of_weak_tricotomy : ∀a,b:F. a≠b → a≤b ∨ b≤a;