-theorem not_eq_zero_one: ∀F:field.0 ≠ 1.
- [2:
- intro;
- apply (not_eq_zero_one_ ? ? ? (field_properties F))
- | skip
- ]
-qed.
-
-definition sum_field ≝
- λF:field. sum ? (plus F) (zero F) (one F).
-
-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;
- (* 0 characteristics *)
- of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
- }.
-
-record ordered_field_ch0 : Type \def
- { of_field:> field;
- of_le: of_field → of_field → Prop;
- of_ordered_field_properties:> is_ordered_field_ch0 of_field of_le
- }.
-
-interpretation "Ordered field le" 'leq a b =
- (cic:/matita/integration_algebras/of_le.con _ a b).
-
-definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b.
-
-interpretation "Ordered field lt" 'lt a b =
- (cic:/matita/integration_algebras/lt.con _ a b).
-
-(*incompleto
-lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F. 0 ≤ x → -x ≤ 0.
-intros;
- generalize in match (of_plus_compat ? ? ? ? ? ? ? ? F ? ? (-x) H); intro;
- rewrite > (zero_neutral ? ? ? ? F) in H1;
- rewrite > (plus_comm ? ? ? ? F) in H1;
- rewrite > (opp_inverse ? ? ? ? F) in H1;
-
- assumption.
-qed.*)
-
-axiom le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
-(* intros;
- generalize in match (of_plus_compat ? ? ? ? ? ? ? ? F ? ? (-x) H); intro;
- rewrite > (zero_neutral ? ? ? ? F) in H1;
- rewrite > (plus_comm ? ? ? ? F) in H1;
- rewrite > (opp_inverse ? ? ? ? F) in H1;
- assumption.
-qed.*)
-
-(*
-lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
- intros;
-
-lemma not_eq_x_zero_to_lt_zero_mult_x_x:
- ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.