Definition AbsSmall (R : COrdField) (e x : R) : Prop := [--]e [<=] x /\ x [<=] e.



Section AbsSmall_properties.

Variable R : COrdField.

Lemma AbsSmall_wdr : rel_wdr R (AbsSmall (R:=R)).

Lemma AbsSmall_wdr_unfolded : forall x y z : R,
 AbsSmall x y -> y [=] z -> AbsSmall x z.

Lemma AbsSmall_wdl : rel_wdl R (AbsSmall (R:=R)).

Lemma AbsSmall_wdl_unfolded : forall x y z : R,
 AbsSmall x y -> x [=] z -> AbsSmall z y.



Lemma AbsSmall_leEq_trans : forall e1 e2 d : R,
 e1 [<=] e2 -> AbsSmall e1 d -> AbsSmall e2 d.

Lemma zero_AbsSmall : forall e : R, 0 [<=] e -> AbsSmall e 0.

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

Lemma AbsSmall_trans : forall e1 e2 d : R,
 e1 [<] e2 -> AbsSmall e1 d -> AbsSmall e2 d.

Lemma leEq_imp_AbsSmall : forall e d : R, 0 [<=] e -> e [<=] d -> AbsSmall d e.

Lemma inv_resp_AbsSmall : forall x y : R, AbsSmall x y -> AbsSmall x [--]y.

Lemma mult_resp_AbsSmall: forall (R: COrdField) (x y e : R) (H: 0[<=]y),
AbsSmall e x -> AbsSmall (y[*]e) (y[*]x).

Lemma div_resp_AbsSmall: forall (R: COrdField) (x y e : R) (H: 0[<]y),
AbsSmall e x -> AbsSmall (e[/]y[//]pos_ap_zero _ _ H) (x[/]y[//]pos_ap_zero _ _ H).

Lemma sum_resp_AbsSmall : forall
(x y : N -> R) (n m: N)
(H1 : m <= n) (H2 : forall i : N, m <= i -> i <= n -> AbsSmall (y i) (x i)),
AbsSmall (∑ m n y) (∑ m n x).





Lemma AbsSmall_minus : forall e x1 x2 : R, AbsSmall e (x1[-]x2) -> AbsSmall e (x2[-]x1).

Lemma AbsSmall_plus : forall e1 e2 x1 x2 : R,
 AbsSmall e1 x1 -> AbsSmall e2 x2 -> AbsSmall (e1[+]e2) (x1[+]x2).

Lemma AbsSmall_eps_div_two : forall e x1 x2 : R,
 AbsSmall (e [/]2) x1 -> AbsSmall (e [/]2) x2 -> AbsSmall e (x1[+]x2).

Lemma AbsSmall_x_plus_delta : forall x ε δ : R,
 0 [<=] ε -> 0 [<=] δ -> δ [<=] ε -> AbsSmall ε (x[-] (x[+]δ)).

Lemma AbsSmall_x_minus_delta : forall x ε δ : R,
 0 [<=] ε -> 0 [<=] δ -> δ [<=] ε -> AbsSmall ε (x[-] (x[-]δ)).

Lemma AbsSmall_x_plus_eps_div2 : forall x ε : R, 0 [<=] ε -> AbsSmall ε (x[-] (x[+]ε [/]2)).

Lemma AbsSmall_x_minus_eps_div2 : forall x ε : R, 0 [<=] ε -> AbsSmall ε (x[-] (x[-]ε [/]2)).

Lemma AbsSmall_intermediate : forall x y z ε : R,
 x [<=] y -> y [<=] z -> AbsSmall ε (z[-]x) -> AbsSmall ε (z[-]y).

Lemma AbsSmall_eps_div2 : forall ε : R, 0 [<=] ε -> AbsSmall ε (ε [/]2).

Lemma AbsSmall_nonneg : forall e x : R, AbsSmall e x -> 0 [<=] e.

Lemma AbsSmall_mult : forall e1 e2 x1 x2 : R,
 AbsSmall e1 x1 -> AbsSmall e2 x2 -> AbsSmall (3[*] (e1[*]e2)) (x1[*]x2).

Lemma AbsSmall_cancel_mult : forall e x z : R,
 0 [<] z -> AbsSmall (e[*]z) (x[*]z) -> AbsSmall e x.

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

Lemma mult_AbsSmall'_rht : forall x y C : R, 0 [<=] C ->
 [--]C [<=] x -> x [<=] C -> [--]C [<=] y -> y [<=] C -> x[*]y [<=] 3[*]C[^]2.






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

Lemma mult_AbsSmall_lft : forall x y X Y : R, 0 [<=] X -> 0 [<=] Y ->
 [--]X [<=] x -> x [<=] X -> [--]Y [<=] y -> y [<=] Y -> [--](X[*]Y) [<=] x[*]y.



Lemma mult_AbsSmall : forall x y X Y : R,
 AbsSmall X x -> AbsSmall Y y -> AbsSmall (X[*]Y) (x[*]y).



End AbsSmall_properties.

Definition absBig (R : COrdField) (e x : R) : CProp :=
 0 [<] e and (e [<=] x or x [<=] [--]e).

Notation AbsBig := (absBig _).

Lemma AbsBigSmall_minus : forall (R : COrdField) (e1 e2 x1 x2 : R),
 e2 [<] e1 -> AbsBig e1 x1 -> AbsSmall e2 x2 -> AbsBig (e1[-]e2) (x1[-]x2).

Section absBig_wd_properties.

Variable R : COrdField.

Lemma AbsBig_wdr : Crel_wdr R AbsBig.

Lemma AbsBig_wdl : Crel_wdl R AbsBig.

Lemma AbsBig_wdr_unfolded : forall x y z : R, AbsBig x y -> y [=] z -> AbsBig x z.

Lemma AbsBig_wdl_unfolded : forall x y z : R, AbsBig x y -> x [=] z -> AbsBig z y.

End absBig_wd_properties.


Add Parametric Morphism c : (@AbsSmall c) with signature (@cs_eq (cof_crr c)) ==> (@cs_eq c) ==> iff as AbsSmall_morph_wd.
Qed.