Section Properties_of_leEq.

Properties of ≤

Let R be an ordered field.

Variable R : COrdField.

Section addition.

Addition and subtraction


Lemma plus_resp_leEq : forall x y z : R, x [<=] y -> x[+]z [<=] y[+]z.

Lemma plus_resp_leEq_lft : forall x y z : R, x [<=] y -> z[+]x [<=] z[+]y.

Lemma minus_resp_leEq : forall x y z : R, x [<=] y -> x[-]z [<=] y[-]z.

Lemma inv_resp_leEq : forall x y : R, x [<=] y -> [--]y [<=] [--]x.

Lemma minus_resp_leEq_rht : forall x y z : R, y [<=] x -> z[-]x [<=] z[-]y.

Lemma plus_resp_leEq_both : forall x y a b : R, x [<=] y -> a [<=] b -> x[+]a [<=] y[+]b.

Lemma plus_resp_less_leEq : forall a b c d : R, a [<] b -> c [<=] d -> a[+]c [<] b[+]d.



Lemma plus_resp_leEq_less : forall a b c d : R, a [<=] b -> c [<] d -> a[+]c [<] b[+]d.

Lemma plus_resp_nonneg : forall x y : R, 0 [<=] x -> 0 [<=] y -> 0 [<=] x[+]y.

Lemma minus_resp_less_leEq : forall x y x' y' : R, x [<=] y -> y' [<] x' -> x[-]x' [<] y[-]y'.


Lemma minus_resp_leEq_both : forall x y x' y' : R, x [<=] y -> y' [<=] x' -> x[-]x' [<=] y[-]y'.



Cancellation properties

Lemma plus_cancel_leEq_rht : forall x y z : R, x[+]z [<=] y[+]z -> x [<=] y.

Lemma inv_cancel_leEq : forall x y : R, [--]y [<=] [--]x -> x [<=] y.

Laws for shifting

Lemma shift_plus_leEq : forall a b c : R, a [<=] c[-]b -> a[+]b [<=] c.

Lemma shift_leEq_plus : forall a b c : R, a[-]b [<=] c -> a [<=] c[+]b.

Lemma shift_plus_leEq' : forall a b c : R, b [<=] c[-]a -> a[+]b [<=] c.

Lemma shift_leEq_plus' : forall a b c : R, a[-]b [<=] c -> a [<=] b[+]c.


Lemma shift_leEq_rht : forall a b : R, 0 [<=] b[-]a -> a [<=] b.


Lemma shift_leEq_lft : forall a b : R, a [<=] b -> 0 [<=] b[-]a.


Lemma shift_minus_leEq : forall a b c : R, a [<=] c[+]b -> a[-]b [<=] c.

Lemma shift_leEq_minus : forall a b c : R, a[+]c [<=] b -> a [<=] b[-]c.

Lemma shift_leEq_minus' : forall a b c : R, c[+]a [<=] b -> a [<=] b[-]c.

Lemma shift_zero_leEq_minus : forall x y : R, x [<=] y -> 0 [<=] y[-]x.

Lemma shift_zero_leEq_minus' : forall x y : R, 0 [<=] y[-]x -> x [<=] y.

End addition.

Section multiplication.

Multiplication and division



Multiplication and division respect ≤

Lemma mult_resp_leEq_rht : forall x y z : R, x [<=] y -> 0 [<=] z -> x[*]z [<=] y[*]z.

Lemma mult_resp_leEq_lft : forall x y z : R, x [<=] y -> 0 [<=] z -> z[*]x [<=] z[*]y.

Lemma mult_resp_leEq_both : forall x x' y y' : R,
 0 [<=] x -> 0 [<=] y -> x [<=] x' -> y [<=] y' -> x[*]y [<=] x'[*]y'.

Lemma recip_resp_leEq : forall (x y : R) x_ y_, 0 [<] y -> y [<=] x -> (1[/] x[//]x_) [<=] (1[/] y[//]y_).






Lemma div_resp_leEq : forall (x y z : R) z_, 0 [<] z -> x [<=] y -> (x[/] z[//]z_) [<=] (y[/] z[//]z_).


Cancellation properties

Lemma mult_cancel_leEq : forall x y z : R, 0 [<] z -> x[*]z [<=] y[*]z -> x [<=] y.

Laws for shifting

Lemma shift_mult_leEq : forall (x y z : R) z_, 0 [<] z -> x [<=] (y[/] z[//]z_) -> x[*]z [<=] y.

Lemma shift_mult_leEq' : forall (x y z : R) z_, 0 [<] z -> x [<=] (y[/] z[//]z_) -> z[*]x [<=] y.

Lemma shift_leEq_mult' : forall (x y z : R) y_, 0 [<] y -> (x[/] y[//]y_) [<=] z -> x [<=] y[*]z.




Lemma shift_div_leEq : forall x y z : R, 0 [<] z -> forall z_ : z [#] 0, x [<=] y[*]z -> (x[/] z[//]z_) [<=] y.

Lemma shift_div_leEq' : forall (x y z : R) z_, 0 [<] z -> x [<=] z[*]y -> (x[/] z[//]z_) [<=] y.

Lemma shift_leEq_div : forall (x y z : R) y_, 0 [<] y -> x[*]y [<=] z -> x [<=] (z[/] y[//]y_).



Lemma eps_div_leEq_eps : forall (ε d : R) d_, 0 [<=] ε -> 1 [<=] d -> (ε[/] d[//]d_) [<=] ε.

Lemma nonneg_div_two : forall ε : R, 0 [<=] ε -> 0 [<=] ε [/]2.

Lemma nonneg_div_two' : forall ε : R, 0 [<=] ε -> ε [/]2 [<=] ε.

Lemma nonneg_div_three : forall ε : R, 0 [<=] ε -> 0 [<=] ε [/]3.

Lemma nonneg_div_three' : forall ε : R, 0 [<=] ε -> ε [/]3 [<=] ε.

Lemma nonneg_div_four : forall ε : R, 0 [<=] ε -> 0 [<=] ε [/]4.

Lemma nonneg_div_four' : forall ε : R, 0 [<=] ε -> ε [/]4 [<=] ε.

End multiplication.

Section misc.

Miscellaneous Properties


Lemma sqr_nonneg : forall x : R, 0 [<=] x[^]2.







Lemma nring_nonneg : forall n : N, 0 [<=] nring (R:=R) n.

Lemma suc_leEq_dub : forall n, nring (R:=R) (S (S n)) [<=] 2[*]nring (S n).

Lemma leEq_nring : forall n m, nring (R:=R) n [<=] nring m -> n <= m.

Lemma cc_abs_aid : forall x y : R, 0 [<=] x[^]2[+]y[^]2.


Lemma nexp_resp_pos : forall (x : R) k, 0 [<] x -> 0 [<] x[^]k.


Lemma mult_resp_nonneg : forall x y : R, 0 [<=] x -> 0 [<=] y -> 0 [<=] x[*]y.











Lemma nexp_resp_nonneg : forall (x : R) (k : N), 0 [<=] x -> 0 [<=] x[^]k.



Lemma power_resp_leEq : forall (x y : R) k, 0 [<=] x -> x [<=] y -> x[^]k [<=] y[^]k.




Lemma nexp_resp_less : forall (x y : R) n, 1 <= n -> 0 [<=] x -> x [<] y -> x[^]n [<] y[^]n.

Lemma power_cancel_leEq : forall (x y : R) k, 0 < k -> 0 [<=] y -> x[^]k [<=] y[^]k -> x [<=] y.


Lemma power_cancel_less : forall (x y : R) k, 0 [<=] y -> x[^]k [<] y[^]k -> x [<] y.









Lemma nat_less_bin_nexp : forall p : N, Snring R p [<] 2[^]S p.

Lemma Sum_resp_leEq : forall (f g : N -> R) a b, a <= S b ->
 (forall i, a <= i -> i <= b -> f i [<=] g i) -> ∑ a b f [<=] ∑ a b g.









Lemma Sumx_resp_leEq : forall n (f g : forall i, i < n -> R),
 (forall i H, f i H [<=] g i H) -> Sumx f [<=] Sumx g.

Lemma Sum2_resp_leEq : forall m n, m <= S n -> forall f g : forall i, m <= i -> i <= n -> R,
 (forall i Hm Hn, f i Hm Hn [<=] g i Hm Hn) -> ∑2 f [<=] ∑2 g.

Lemma approach_zero : forall x : R, (forall e, 0 [<] e -> x [<] e) -> x [<=] 0.

Lemma approach_zero_weak : forall x : R, (forall e, 0 [<] e -> x [<=] e) -> x [<=] 0.
End misc.

Lemma equal_less_leEq : forall a b x y : R,
 (a [<] b -> x [<=] y) -> (a [=] b -> x [<=] y) -> a [<=] b -> x [<=] y.

Lemma power_plus_leEq : forall n (x y:R), (0 < n) -> (0[<=]x) -> (0[<=]y) ->
(x[^]n [+] y[^]n)[<=](x[+]y)[^]n.

End Properties_of_leEq.


Section PosP_properties.

Properties of positive numbers

Let R be an ordered field.
Variable R : COrdField.


Lemma mult_pos_imp : forall a b : R, 0 [<] a[*]b -> 0 [<] a and 0 [<] b or a [<] 0 and b [<] 0.

Lemma plus_resp_pos_nonneg : forall x y : R, 0 [<] x -> 0 [<=] y -> 0 [<] x[+]y.



Lemma plus_resp_nonneg_pos : forall x y : R, 0 [<=] x -> 0 [<] y -> 0 [<] x[+]y.

Lemma pos_square : forall x : R, x [#] 0 -> 0 [<] x[^]2.



Lemma mult_cancel_pos_rht : forall x y : R, 0 [<] x[*]y -> 0 [<=] x -> 0 [<] y.

Lemma mult_cancel_pos_lft : forall x y : R, 0 [<] x[*]y -> 0 [<=] y -> 0 [<] x.


Lemma pos_wd : forall x y : R, x [=] y -> 0 [<] y -> 0 [<] x.

Lemma even_power_pos : forall n, even n -> forall x : R, x [#] 0 -> 0 [<] x[^]n.




Lemma odd_power_cancel_pos : forall n, odd n -> forall x : R, 0 [<] x[^]n -> 0 [<] x.





Lemma plus_resp_pos : forall x y : R, 0 [<] x -> 0 [<] y -> 0 [<] x[+]y.


Lemma pos_nring_S : forall n, ZeroR [<] nring (S n).

Lemma square_eq_pos : forall x a : R, 0 [<] a -> 0 [<] x -> x[^]2 [=] a[^]2 -> x [=] a.

Lemma square_eq_neg : forall x a : R, 0 [<] a -> x [<] 0 -> x[^]2 [=] a[^]2 -> x [=] [--]a.

End PosP_properties.


Properties of one over successor

Let R be an ordered field.

Definition one_div_succ (R : COrdField) i : R := 1[/] Snring R i[//]nringS_ap_zero _ i.


Section One_div_succ_properties.

Variable R : COrdField.

Lemma one_div_succ_resp_leEq : forall m n, m <= n -> one_div_succ (R:=R) n [<=] one_div_succ m.


Lemma one_div_succ_pos : forall i, (0:R) [<] one_div_succ i.

Lemma one_div_succ_resp_less : forall i j, i < j -> one_div_succ j [<] one_div_succ (R:=R) i.


End One_div_succ_properties.

Properties of ½


Definition ½ (R : COrdField) := (1:R) [/]2.


Section Half_properties.

Let R be an ordered field.

Variable R : COrdField.

Lemma half_1 : (½:R) [*]2 [=] 1.

Lemma pos_half : (0:R) [<] ½.

Lemma half_1' : forall x : R, x[*]½[*]2 [=] x.

Lemma half_2 : (½:R) [+]½ [=] 1.

Lemma half_lt1 : (½:R) [<] 1.

Lemma half_3 : forall x : R, 0 [<] x -> ½[*]x [<] x.

End Half_properties.