record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
{ of_total_order_relation:> is_total_order_relation ? le;
of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def
{ of_total_order_relation:> is_total_order_relation ? le;
of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b);
axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → 0 < sum_field F n.
axiom lt_zero_to_le_inv_zero:
axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → 0 < sum_field F n.
axiom lt_zero_to_le_inv_zero:
- ∀n:nat.∃m:nat.∀j:nat. le m j →
- l - (inv F (sum_field F (S n)) ?) ≤ f j ∧
- f j ≤ l + (inv F (sum_field F (S n)) ?));
+ ∀n:nat.∃m:nat.∀j:nat. m≤j →
+ l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
+ f j ≤ l + (inv F (sum_field ? (S n)) ?));