(**
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/

(* Goal: F (fun x : T => P (g x)) *)
Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
(* Goal: F (fun x : T => P (g x)) *)
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
(* Goal: F (fun x : T => P (g x)) *)
Copyright (C) 2011-2015 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

Require Import Reals Psatz.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Rbar Rcomplements Hierarchy.

(** This file gives definitions of equivalent (g ~ f) and dominant (g
= o(f)). This is used for defining differentiability on a
[NormedModule]. *)

Definition is_domin {T} {Ku Kv : AbsRing}
  {U : NormedModule Ku} {V : NormedModule Kv}
(* Goal: F (fun x : T => P (g x)) *)
  (F : (T -> Prop) -> Prop) (f : T -> U) (g : T -> V) :=
  forall eps : posreal, F (fun x => norm (g x) <= eps * norm (f x)).

Definition is_equiv {T} {K : AbsRing} {V : NormedModule K}
(* Goal: F (fun x : T => P (g x)) *)
  (F : (T -> Prop) -> Prop) (f g : T -> V) :=
  is_domin F g (fun x => minus (g x) (f x)).

(** To be dominant is a partial strict order *)

Lemma domin_antisym {T} {K : AbsRing} {V : NormedModule K} :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : ProperFilter F} (f : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  F (fun x => norm (f x) <> 0) -> ~ is_domin F f f.
Proof.
(* Goal: forall (F : forall _ : forall _ : T, Prop, Prop) (_ : @ProperFilter T F) (f : forall _ : T, NormedModule.sort K V) (_ : F (fun x : T => not (@eq R (@norm K V (f x)) (IZR Z0)))), not (@is_domin T K K V V F f f) *)
intros F FF f Hf H.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
move: (H (pos_div_2 (mkposreal _ Rlt_0_1))) => {H} /= H.
(* Goal: False *)
apply filter_const.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
generalize (filter_and _ _ H Hf) => {H Hf}.
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
apply filter_imp.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (Rinv (IZR (Zpos (xO xH)))) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
intros x [H1 H2].
(* Goal: False *)
generalize (norm_ge_0 (f x)).
(* Goal: forall (_ : Rle (IZR Z0) (@norm R_AbsRing R_NormedModule (g x))) (_ : forall _ : @eq R (@norm R_AbsRing R_NormedModule (g x)) (IZR Z0), @eq R (g x) (IZR Z0)), not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
lra.
Qed.

Lemma domin_trans {T} {Ku Kv Kw : AbsRing}
   {U : NormedModule Ku} {V : NormedModule Kv} {W : NormedModule Kw} :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g : T -> V) (h : T -> W),
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f g -> is_domin F g h -> is_domin F f h.
Proof.
(* Goal: forall (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f : forall _ : T, NormedModule.sort Ku U) (g : forall _ : T, NormedModule.sort Kv V) (h : forall _ : T, NormedModule.sort Kw W) (_ : @is_domin T Ku Kv U V F f g) (_ : @is_domin T Kv Kw V W F g h), @is_domin T Ku Kw U W F f h *)
  intros F FF f g h Hfg Hgh eps.
(* Goal: F (fun x : T => Rle (@norm Kw W (h x)) (Rmult (pos eps) (@norm Ku U (f x)))) *)
  apply (filter_imp (fun x => (norm (h x) <= sqrt eps * norm (g x)) /\ (norm (g x) <= sqrt eps * norm (f x)))).
(* Goal: forall (x : T) (_ : and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))), Rle (@norm Kw W (h x)) (Rmult (pos eps) (@norm Ku U (f x))) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  intros x [H0 H1].
(* Goal: Rle (@norm Kw W (h x)) (Rmult (pos eps) (@norm Ku U (f x))) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  apply Rle_trans with (1 := H0).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite -{2}(sqrt_sqrt eps).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Rmult_assoc.
(* Goal: Rle (Rmult (sqrt (pos eps)) (@norm Kv V (g x))) (Rmult (sqrt (pos eps)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x)))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  apply Rmult_le_compat_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply sqrt_pos.
(* Goal: Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  apply H1.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, eps.
(* Goal: F (fun x : T => and (Rle (@norm K V (g x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (f x)))) (Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))))) *)
  apply filter_and.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply (Hgh (mkposreal (sqrt eps) (sqrt_lt_R0 _ (cond_pos eps)))).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply (Hfg (mkposreal (sqrt eps) (sqrt_lt_R0 _ (cond_pos eps)))).
Qed.

(** Relations between domination and equivalence *)

Lemma equiv_le_2 {T} {K : AbsRing} {V : NormedModule K}
(* Goal: F (fun x : T => P (g x)) *)
  F {FF : Filter F} (f g : T -> V) :
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f g ->
  F (fun x => norm (g x) <= 2 * norm (f x) /\ norm (f x) <= 2 * norm (g x)).
Proof.
(* Goal: forall _ : Rle (g x) (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)), Rlt (g x) eps *)
  intros H.
(* Goal: F (fun x : T => and (Rle (@norm K V (g x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (f x)))) (Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))))) *)
  apply filter_and.
(* Goal: F (fun x : T => P (g x)) *)
  - move: (H (pos_div_2 (mkposreal _ Rlt_0_1))) => {H}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    apply filter_imp => x /= H.
(* Goal: Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))) *)
    apply Rle_trans with (1 := norm_triangle_inv _ _) in H.
(* Goal: F (fun x : T => P (g x)) *)
    rewrite -Ropp_minus_distr Rabs_Ropp in H.
(* Goal: Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))) *)
    apply Rabs_le_between' in H ; case: H => H _.
(* Goal: Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))) *)
    field_simplify in H.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
    rewrite Rdiv_1 in H.
(* Goal: Rle (@norm K V (g x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (f x))) *)
(* Goal: F (fun x : T => Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x)))) *)
    apply Rle_div_l in H.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by rewrite Rmult_comm.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by apply Rlt_0_2.
(* Goal: F (fun x : T => P (g x)) *)
  - move: (H (mkposreal _ Rlt_0_1)) => {H}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    apply filter_imp => x /= H.
(* Goal: Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))) *)
    apply Rle_trans with (1 := norm_triangle_inv _ _) in H.
(* Goal: F (fun x : T => P (g x)) *)
    rewrite -Ropp_minus_distr Rabs_Ropp in H.
(* Goal: Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))) *)
    apply Rabs_le_between' in H ; case: H => _ H.
(* Goal: Rle (@norm K V (f x)) (Rmult (IZR (Zpos (xO xH))) (@norm K V (g x))) *)
    field_simplify in H.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by rewrite !Rdiv_1 in H.
Qed.

Lemma domin_rw_l {T} {Ku Kv : AbsRing}
  {U : NormedModule Ku} {V : NormedModule Kv} :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f1 f2 : T -> U) (g : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f1 f2 -> is_domin F f1 g -> is_domin F f2 g.
Proof.
  intros F FF f1 f2 g Hf Hg eps.
  assert (F (fun x => norm (f1 x) <= 2 * norm (f2 x))).
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
    eapply filter_imp.
    2: apply (equiv_le_2 _ _ _ Hf).
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
    move => /= x Hx.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by apply Hx.
  clear Hf ; rename H into Hf.
  specialize (Hg (pos_div_2 eps)).
(* Goal: F (fun x : T => P (g x)) *)
  generalize (filter_and _ _ Hf Hg) ; clear -FF.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x /= [Hf Hg].
  apply Rle_trans with (1 := Hg).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /Rdiv Rmult_assoc.
(* Goal: Rle (Rmult (sqrt (pos eps)) (@norm Kv V (g x))) (Rmult (sqrt (pos eps)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x)))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  apply Rmult_le_compat_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, eps.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Rmult_comm Rle_div_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by rewrite Rmult_comm.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_0_2.
Qed.

Lemma domin_rw_r {T} {Ku Kv : AbsRing}
  {U : NormedModule Ku} {V : NormedModule Kv} :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g1 g2 : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F g1 g2 -> is_domin F f g1 -> is_domin F f g2.
Proof.
  intros F FF f g1 g2 Hg Hf eps.
  assert (F (fun x => norm (g2 x) <= 2 * norm (g1 x))).
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
    eapply filter_imp.
    2: apply (equiv_le_2 _ _ _ Hg).
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
    move => /= x Hx.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by apply Hx.
  clear Hg ; rename H into Hg.
  specialize (Hf (pos_div_2 eps)).
(* Goal: F (fun x : T => P (g x)) *)
  generalize (filter_and _ _ Hf Hg) ; clear -FF.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x /= [Hf Hg].
  apply Rle_trans with (1 := Hg).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Rmult_comm Rle_div_r.
  apply Rle_trans with (1 := Hf).
  right ; rewrite /Rdiv ; ring.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_0_2.
Qed.

(** To be equivalent is an equivalence relation *)

Section Equiv.

Context {T : Type} {K : AbsRing} {V : NormedModule K}.

Lemma equiv_refl :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> V),
  is_equiv F f f.
Proof.
(* Goal: forall (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f : forall _ : T, NormedModule.sort K V), @is_equiv T K V F f f *)
  intros F FF f eps.
(* Goal: F (fun x : T => Rle (@norm K V (@minus (NormedModule.AbelianGroup K V) (f x) (f x))) (Rmult (pos eps) (@norm K V (f x)))) *)
  apply: filter_forall => x.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /minus plus_opp_r norm_zero.
(* Goal: Rle (IZR Z0) (Rmult (pos eps) (@norm K V (g x))) *)
  apply Rmult_le_pos.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, eps.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply norm_ge_0.
Qed.

Lemma equiv_sym :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f g -> is_equiv F g f.
Proof.
  intros F FF f g H eps.
  assert (H0 := equiv_le_2 _ _ _ H).
  specialize (H (pos_div_2 eps)).
  generalize (filter_and _ _ H H0) ; apply filter_imp ;
  clear => x [H [H0 H1]].
(* Goal: F (fun x : T => P (g x)) *)
  rewrite -norm_opp /minus opp_plus opp_opp plus_comm.
  apply Rle_trans with (1 := H) ; simpl.
  eapply Rle_trans.
(* Goal: Rle (Rmult (sqrt (pos eps)) (@norm Kv V (g x))) (Rmult (sqrt (pos eps)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x)))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  apply Rmult_le_compat_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, is_pos_div_2.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply H0.
  apply Req_le ; field.
Qed.

Lemma equiv_trans :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g h : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f g -> is_equiv F g h -> is_equiv F f h.
Proof.
  intros F FF f g h Hfg Hgh.
  apply (fun c => domin_rw_l _ _ c Hgh).
(* Goal: @is_domin T Ku Kv U V G f g *)
  intros eps.
  apply equiv_sym in Hgh.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  generalize (filter_and _ _ (Hfg (pos_div_2 eps)) (Hgh (pos_div_2 eps))) => {Hfg Hgh}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x /= [Hfg Hgh].
  replace (minus (h x) (f x)) with (plus (minus (g x) (f x)) (opp (minus (g x) (h x)))).
  eapply Rle_trans. 1 : by apply @norm_triangle.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite norm_opp (double_var eps) Rmult_plus_distr_r.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rplus_le_compat.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /minus opp_plus opp_opp plus_comm plus_assoc.
  congr (plus _ (opp (f x))).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite plus_comm plus_assoc plus_opp_r.
  apply plus_zero_l.
Qed.

Lemma equiv_carac_0 :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f g ->
(* Goal: F (fun x : T => P (g x)) *)
  {o : T -> V | (forall x : T, f x = plus (g x) (o x)) /\ is_domin F g o }.
Proof.
(* Goal: forall (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f g : forall _ : T, NormedModule.sort K V) (_ : @is_equiv T K V F f g), @sig (forall _ : T, NormedModule.sort K V) (fun o : forall _ : T, NormedModule.sort K V => and (forall x : T, @eq (NormedModule.sort K V) (f x) (@plus (NormedModule.AbelianGroup K V) (g x) (o x))) (@is_domin T K K V V F g o)) *)
  intros F FF f g H.
(* Goal: @sig (forall _ : T, NormedModule.sort K V) (fun o : forall _ : T, NormedModule.sort K V => and (forall x : T, @eq (NormedModule.sort K V) (f x) (@plus (NormedModule.AbelianGroup K V) (g x) (o x))) (@is_domin T K K V V F g o)) *)
  exists (fun x => minus (f x) (g x)).
(* Goal: ineqs x *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  split.
(* Goal: forall x : T, @eq (NormedModule.sort K V) (f x) (@plus (NormedModule.AbelianGroup K V) (g x) (@minus (NormedModule.AbelianGroup K V) (f x) (g x))) *)
(* Goal: @is_domin T K K V V F g (fun x : T => @minus (NormedModule.AbelianGroup K V) (f x) (g x)) *)
  intro x.
(* Goal: F (fun x : T => P (g x)) *)
  by rewrite /minus plus_comm -plus_assoc plus_opp_l plus_zero_r.
(* Goal: @is_domin T K K V V F g (fun x : T => @minus (NormedModule.AbelianGroup K V) (f x) (g x)) *)
  apply (domin_rw_l _ _ _ H).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply equiv_sym.
Qed.

Lemma equiv_carac_1 :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g o : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  (forall x, f x = plus (g x) (o x)) -> is_domin F g o -> is_equiv F f g.
Proof.
  intros F FF f g o Ho Hgo.
  intro eps ; move: (Hgo eps).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x.
  replace (o x) with (minus (f x) (g x)).
  congr (_ <= _).
(* Goal: F (fun x : T => P (g x)) *)
  by rewrite -norm_opp /minus opp_plus opp_opp plus_comm.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Ho.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /minus plus_comm plus_assoc plus_opp_l.
  apply plus_zero_l.
Qed.

(* Goal: F (fun x : T => P (g x)) *)
Lemma equiv_ext_loc {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V) :
(* Goal: F (fun x : T => P (g x)) *)
  F (fun x => f x = g x) -> is_equiv F f g.
Proof.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move => H eps.
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
  move: H ; apply filter_imp.
(* Goal: F (fun x : T => P (g x)) *)
  move => x ->.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /minus plus_opp_r norm_zero.
(* Goal: Rle (IZR Z0) (Rmult (pos eps) (@norm K V (g x))) *)
  apply Rmult_le_pos.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, eps.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply norm_ge_0.
Qed.

End Equiv.

(** * Vector space *)
(** is_domin is a vector space *)

Section Domin.

Context {T : Type} {Ku Kv : AbsRing}
  {U : NormedModule Ku} {V : NormedModule Kv}.

(* Goal: F (fun x : T => P (g x)) *)
Lemma is_domin_le {F G} (f : T -> U) (g : T -> V) :
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f g -> filter_le G F -> is_domin G f g.
Proof.
(* Goal: forall (_ : @is_domin T Ku Kv U V F f g) (_ : @filter_le T G F), @is_domin T Ku Kv U V G f g *)
  intros.
(* Goal: @is_domin T Ku Kv U V G f g *)
  intros eps.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply H0.
Qed.

Lemma domin_scal_r  :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g : T -> V) (c : Kv),
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f g -> is_domin F f (fun x => scal c (g x)).
Proof.
  intros F FF f g c H.
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  case: (Req_dec (abs c) 0) => Hc.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move => eps /=.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp with (2 := filter_true) => x _.
  eapply Rle_trans.
  apply @norm_scal.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Hc Rmult_0_l.
(* Goal: Rle (IZR Z0) (Rmult (pos eps) (@norm K V (g x))) *)
  apply Rmult_le_pos.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, eps.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply norm_ge_0.

(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  destruct (abs_ge_0 c) => //.
  clear Hc ; rename H0 into Hc.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move => eps /=.
  assert (He : 0 < eps / abs c).
(* Goal: Rlt (IZR Z0) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
    apply Rdiv_lt_0_compat.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by apply eps.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by apply Hc.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move: (H (mkposreal _ He)) => /= {H}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x H.
  eapply Rle_trans.
  apply @norm_scal.
  rewrite Rmult_comm ; apply Rle_div_r.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by [].
  apply Rle_trans with (1 := H).
  apply Req_le ; rewrite /Rdiv ; ring.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply sym_eq in H0.
Qed.

Lemma domin_scal_l :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g : T -> V) (c : Ku),
(* Goal: F (fun x : T => P (g x)) *)
  (exists y, mult y c = one) -> is_domin F f g -> is_domin F (fun x => scal c (f x)) g.
Proof.
  intros F FF f g c Hc H eps.
  destruct Hc as [y Hc].
  assert (0 < abs c).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    apply Rnot_le_lt => H0.
    destruct H0.
    move: H0 ; by apply Rle_not_lt, abs_ge_0.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
    move: H0.
    apply (Rmult_neq_0_reg (abs y)).
(* Goal: not (@eq R (Rplus (Rabs l) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
    apply Rgt_not_eq.
    eapply Rlt_le_trans, @abs_mult.
    rewrite Hc abs_one ; by apply Rlt_0_1.
  assert (0 < abs y).
    apply Rmult_lt_reg_r with (abs c).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by [].
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
    rewrite Rmult_0_l.
    eapply Rlt_le_trans, @abs_mult.
    rewrite Hc abs_one ; by apply Rlt_0_1.
  assert (He : (0 < eps / abs y)).
(* Goal: Rlt (IZR Z0) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
    apply Rdiv_lt_0_compat.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by apply eps.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by [].
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move: (H (mkposreal _ He)) => /= {H}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x Hx.
  apply Rle_trans with (1 := Hx).
(* Goal: Rle (Rmult (sqrt (pos eps)) (@norm Kv V (g x))) (Rmult (sqrt (pos eps)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x)))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  rewrite /Rdiv Rmult_assoc ; apply Rmult_le_compat_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, eps.
(* Goal: F (fun x : T => P (g x)) *)
  rewrite -{1}(scal_one (f x)) -Hc -scal_assoc.
  eapply Rle_trans.
(* Goal: Rle (Rmult (sqrt (pos eps)) (@norm Kv V (g x))) (Rmult (sqrt (pos eps)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x)))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  apply Rmult_le_compat_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rlt_le, Rinv_0_lt_compat.
  apply @norm_scal.
  apply Req_le ; field.
(* Goal: not (@eq R (Rplus (Rabs l) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  by apply Rgt_not_eq.
Qed.

Lemma domin_plus :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g1 g2 : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f g1 -> is_domin F f g2 -> is_domin F f (fun x => plus (g1 x) (g2 x)).
Proof.
  intros F FF f g1 g2 Hg1 Hg2 eps.
  generalize (filter_and _ _ (Hg1 (pos_div_2 eps)) (Hg2 (pos_div_2 eps)))
    => /= {Hg1 Hg2}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x [Hg1 Hg2].
  eapply Rle_trans.
  apply @norm_triangle.
  eapply Rle_trans.
  apply Rplus_le_compat.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Hg1.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Hg2.
  apply Req_le ; field.
Qed.

End Domin.

(** is_equiv is compatible with the vector space structure *)

Section Equiv_VS.

Context {T : Type} {K : AbsRing} {V : NormedModule K}.

Lemma equiv_scal :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V) (c : K),
(* Goal: F (fun x : T => P (g x)) *)
  (exists y : K, mult y c = one) ->
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f g -> is_equiv F (fun x => scal c (f x)) (fun x => scal c (g x)).
Proof.
(* Goal: forall (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f g : forall _ : T, NormedModule.sort K V) (c : AbsRing.sort K) (_ : @ex (AbsRing.sort K) (fun y : AbsRing.sort K => @eq (Ring.sort (AbsRing.Ring K)) (@mult (AbsRing.Ring K) y c) (@one (AbsRing.Ring K)))) (_ : @is_equiv T K V F f g), @is_equiv T K V F (fun x : T => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (f x)) (fun x : T => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (g x)) *)
  intros F FF f g c [y Hc] H.
(* Goal: @is_equiv T K V F (fun x : T => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (f x)) (fun x : T => @scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (g x)) *)
  apply domin_scal_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by exists y.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move => eps /=.
(* Goal: F (fun x : T => Rle (@norm K V (@minus (NormedModule.AbelianGroup K V) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (g x)) (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (f x)))) (Rmult (pos eps) (@norm K V (g x)))) *)
  cut (F (fun x => norm (scal c (minus (g x) (f x))) <= eps * norm (g x))).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x.
(* Goal: Rle (@norm K V (@minus (NormedModule.AbelianGroup K V) (f x) (@plus (NormedModule.AbelianGroup K V) (f x) (o x)))) (Rmult (pos eps) (@norm K V (f x))) *)
  now rewrite scal_distr_l scal_opp_r.
(* Goal: F (fun x : T => Rle (@norm K V (@scal (AbsRing.Ring K) (NormedModule.ModuleSpace K V) c (@minus (NormedModule.AbelianGroup K V) (g x) (f x)))) (Rmult (pos eps) (@norm K V (g x)))) *)
  now apply domin_scal_r.
Qed.

Lemma equiv_plus :
(* Goal: F (fun x : T => P (g x)) *)
  forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f o : T -> V),
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f o -> is_equiv F (fun x => plus (f x) (o x)) f.
Proof.
(* Goal: forall (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f o : forall _ : T, NormedModule.sort K V) (_ : @is_domin T K K V V F f o), @is_equiv T K V F (fun x : T => @plus (NormedModule.AbelianGroup K V) (f x) (o x)) f *)
  intros F FF f o H eps.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move: (H eps) => {H}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x Hx.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
  simpl.
(* Goal: Rle (@norm K V (@minus (NormedModule.AbelianGroup K V) (f x) (@plus (NormedModule.AbelianGroup K V) (f x) (o x)))) (Rmult (pos eps) (@norm K V (f x))) *)
  now rewrite /minus opp_plus plus_assoc plus_opp_r plus_zero_l norm_opp.
Qed.

End Equiv_VS.

(** * Multiplication and inverse *)
(** Domination *)

Lemma domin_mult_r :
(* Goal: F (fun x : T => P (g x)) *)
  forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g h : T -> R),
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f g -> is_domin F (fun x => f x * h x) (fun x => g x * h x).
Proof.
(* Goal: forall (T : Type) (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f g h : forall _ : T, R) (_ : @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F f g), @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F (fun x : T => Rmult (f x) (h x)) (fun x : T => Rmult (g x) (h x)) *)
  intros T F FF f g h H eps.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move: (H eps) => {H}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x H1.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /norm /= /abs /= ?Rabs_mult.
(* Goal: F (fun x : T => P (g x)) *)
  rewrite -Rmult_assoc.
(* Goal: Rle (Rdiv (Rabs (g x)) (Rmult (Rabs (f x)) (Rabs (g x)))) (Rdiv (Rmult (pos eps) (Rabs (f x))) (Rmult (Rabs (f x)) (Rabs (g x)))) *)
  apply Rmult_le_compat_r.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rabs_pos.
(* Goal: Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  by apply H1.
Qed.

Lemma domin_mult_l :
(* Goal: F (fun x : T => P (g x)) *)
  forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g h : T -> R),
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f g -> is_domin F (fun x => h x * f x) (fun x => h x * g x).
Proof.
(* Goal: forall (T : Type) (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f g h : forall _ : T, R) (_ : @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F f g), @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F (fun x : T => Rmult (f x) (h x)) (fun x : T => Rmult (g x) (h x)) *)
  intros T F FF f g h H eps.
  generalize (domin_mult_r f g h H eps).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by rewrite ?(Rmult_comm (h x)).
Qed.

Lemma domin_mult :
(* Goal: F (fun x : T => P (g x)) *)
  forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f1 f2 g1 g2 : T -> R),
(* Goal: F (fun x : T => P (g x)) *)
  is_domin F f1 g1 -> is_domin F f2 g2 ->
  is_domin F (fun x => f1 x * f2 x) (fun x => g1 x * g2 x).
Proof.
(* Goal: forall (T : Type) (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f1 f2 g1 g2 : forall _ : T, R) (_ : @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F f1 g1) (_ : @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F f2 g2), @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F (fun x : T => Rmult (f1 x) (f2 x)) (fun x : T => Rmult (g1 x) (g2 x)) *)
  intros T F FF f1 f2 g1 g2 H1 H2 eps.
  move: (H1 (mkposreal _ (sqrt_lt_R0 _ (cond_pos eps))))
    (H2 (mkposreal _ (sqrt_lt_R0 _ (cond_pos eps)))) => {H1 H2} /= H1 H2.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  generalize (filter_and _ _ H1 H2) => {H1 H2}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x [H1 H2].
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /norm /= /abs /= ?Rabs_mult.
(* Goal: F (fun x : T => P (g x)) *)
  rewrite -(sqrt_sqrt _ (Rlt_le _ _ (cond_pos eps))).
  replace (sqrt eps * sqrt eps * (Rabs (f1 x) * Rabs (f2 x)))
    with ((sqrt eps * Rabs (f1 x))*(sqrt eps * Rabs (f2 x))) by ring.
(* Goal: Rle (Rmult (Rabs (g1 x)) (Rabs (g2 x))) (Rmult (Rmult (sqrt (pos eps)) (Rabs (f1 x))) (Rmult (sqrt (pos eps)) (Rabs (f2 x)))) *)
  apply Rmult_le_compat.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rabs_pos.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rabs_pos.
(* Goal: Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))) *)
(* Goal: Rle (IZR Z0) (pos eps) *)
(* Goal: F (fun x : T => and (Rle (@norm Kw W (h x)) (Rmult (sqrt (pos eps)) (@norm Kv V (g x)))) (Rle (@norm Kv V (g x)) (Rmult (sqrt (pos eps)) (@norm Ku U (f x))))) *)
  by apply H1.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply H2.
Qed.

Lemma domin_inv :
(* Goal: F (fun x : T => P (g x)) *)
  forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> R),
(* Goal: F (fun x : T => P (g x)) *)
  F (fun x => g x <> 0) -> is_domin F f g ->
  is_domin F (fun x => / g x) (fun x => / f x).
Proof.
(* Goal: forall (T : Type) (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f g : forall _ : T, R) (_ : F (fun x : T => not (@eq R (g x) (IZR Z0)))) (_ : @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F f g), @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F (fun x : T => Rinv (g x)) (fun x : T => Rinv (f x)) *)
  intros T F FF f g Hg H eps.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  have Hf : F (fun x => f x <> 0).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    generalize (filter_and _ _ Hg (H (mkposreal _ Rlt_0_1))) => /=.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    apply filter_imp => x {Hg H} [Hg H].
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
    case: (Req_dec (f x) 0) => Hf.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
    rewrite /norm /= /abs /= Hf Rabs_R0 Rmult_0_r in H.
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: F (fun x : T => Rle (@norm R_AbsRing R_NormedModule (Rinv (f x))) (Rmult (pos eps) (@norm R_AbsRing R_NormedModule (Rinv (g x))))) *)
    apply Rlt_not_le in H.
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rabs (g x)) *)
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: F (fun x : T => Rle (@norm R_AbsRing R_NormedModule (Rinv (f x))) (Rmult (pos eps) (@norm R_AbsRing R_NormedModule (Rinv (g x))))) *)
    move => _ ; apply H.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by apply Rabs_pos_lt.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    by [].
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  generalize (filter_and _ _ (H eps) (filter_and _ _ Hf Hg)) => {H Hf Hg}.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply filter_imp => x [H [Hf Hg]].
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  rewrite /norm /= /abs /= ?Rabs_Rinv => //.
  replace (/ Rabs (f x))
    with (Rabs (g x) / (Rabs (f x) * Rabs (g x)))
    by (field ; split ; by apply Rabs_no_R0).
  replace (eps * / Rabs (g x))
    with (eps * Rabs (f x) / (Rabs (f x) * Rabs (g x)))
    by (field ; split ; by apply Rabs_no_R0).
(* Goal: Rle (Rdiv (Rabs (g x)) (Rmult (Rabs (f x)) (Rabs (g x)))) (Rdiv (Rmult (pos eps) (Rabs (f x))) (Rmult (Rabs (f x)) (Rabs (g x)))) *)
  apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Rinv (Rmult (Rabs (f x)) (Rabs (g x)))) *)
(* Goal: Rle (Rabs (g x)) (Rmult (pos eps) (Rabs (f x))) *)
  apply Rlt_le, Rinv_0_lt_compat, Rmult_lt_0_compat ; apply Rabs_pos_lt => //.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply H.
Qed.

(** Equivalence *)

Lemma equiv_mult :
(* Goal: F (fun x : T => P (g x)) *)
  forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f1 f2 g1 g2 : T -> R),
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f1 g1 -> is_equiv F f2 g2 ->
  is_equiv F (fun x => f1 x * f2 x) (fun x => g1 x * g2 x).
Proof.
(* Goal: forall (T : Type) (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f1 f2 g1 g2 : forall _ : T, R) (_ : @is_equiv T R_AbsRing R_NormedModule F f1 g1) (_ : @is_equiv T R_AbsRing R_NormedModule F f2 g2), @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rmult (f1 x) (f2 x)) (fun x : T => Rmult (g1 x) (g2 x)) *)
  intros T F FF f1 f2 g1 g2 H1 H2.
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  case: (equiv_carac_0 _ _ H1) => {H1} o1 [H1 Ho1].
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  case: (equiv_carac_0 _ _ H2) => {H2} o2 [H2 Ho2].
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rmult (f1 x) (f2 x)) (fun x : T => Rmult (g1 x) (g2 x)) *)
  apply equiv_carac_1 with (fun x => o1 x * g2 x + g1 x * o2 x + o1 x * o2 x).
(* Goal: forall x : T, @eq (NormedModule.sort R_AbsRing R_NormedModule) (Rmult (f1 x) (f2 x)) (@plus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (Rmult (g1 x) (g2 x)) (Rplus (Rplus (Rmult (o1 x) (g2 x)) (Rmult (g1 x) (o2 x))) (Rmult (o1 x) (o2 x)))) *)
(* Goal: @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F (fun x : T => Rmult (g1 x) (g2 x)) (fun x : T => Rplus (Rplus (Rmult (o1 x) (g2 x)) (Rmult (g1 x) (o2 x))) (Rmult (o1 x) (o2 x))) *)
  move => x ; rewrite H1 H2 /plus /= ; ring.
(* Goal: @is_domin T R_AbsRing R_AbsRing R_NormedModule R_NormedModule F (fun x : T => Rmult (g1 x) (g2 x)) (fun x : T => Rplus (Rplus (Rmult (o1 x) (g2 x)) (Rmult (g1 x) (o2 x))) (Rmult (o1 x) (o2 x))) *)
  repeat apply @domin_plus => //.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply domin_mult_r.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply domin_mult_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply domin_mult.
Qed.

Lemma equiv_inv :
(* Goal: F (fun x : T => P (g x)) *)
  forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> R),
(* Goal: F (fun x : T => P (g x)) *)
  F (fun x => g x <> 0) -> is_equiv F f g ->
  is_equiv F (fun x => / f x) (fun x => / g x).
Proof.
(* Goal: forall (T : Type) (F : forall _ : forall _ : T, Prop, Prop) (_ : @Filter T F) (f g : forall _ : T, R) (_ : F (fun x : T => not (@eq R (g x) (IZR Z0)))) (_ : @is_equiv T R_AbsRing R_NormedModule F f g), @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  intros T F FF f g Hg H.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  have Hf : F (fun x => f x <> 0).
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    generalize (filter_and _ _ Hg (H (pos_div_2 (mkposreal _ Rlt_0_1)))) => /=.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
    apply filter_imp => x {Hg H} [Hg H].
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
    case: (Req_dec (f x) 0) => Hf //.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
    rewrite /minus /plus /opp /= Hf Ropp_0 Rplus_0_r in H.
(* Goal: not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
    generalize (norm_ge_0 (g x)) (norm_eq_zero (g x)).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
    rewrite /zero /=.
(* Goal: forall (_ : Rle (IZR Z0) (@norm R_AbsRing R_NormedModule (g x))) (_ : forall _ : @eq R (@norm R_AbsRing R_NormedModule (g x)) (IZR Z0), @eq R (g x) (IZR Z0)), not (@eq R (f x) (IZR Z0)) *)
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
    lra.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  apply equiv_sym in H.
(* Goal: @is_equiv T R_AbsRing R_NormedModule F (fun x : T => Rinv (f x)) (fun x : T => Rinv (g x)) *)
  move => eps.
(* Goal: F (fun x : T => Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (Rinv (g x)) (Rinv (f x)))) (Rmult (pos eps) (@norm R_AbsRing R_NormedModule (Rinv (g x))))) *)
  generalize (filter_and _ _ (filter_and _ _ Hf Hg) (H eps)).
(* Goal: F (fun x : T => P (g x)) *)
  clear -FF.
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
  apply filter_imp.
(* Goal: forall (x : T) (_ : and (and (not (@eq R (f x) (IZR Z0))) (not (@eq R (g x) (IZR Z0)))) (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos eps) (@norm R_AbsRing R_NormedModule (f x))))), Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (Rinv (g x)) (Rinv (f x)))) (Rmult (pos eps) (@norm R_AbsRing R_NormedModule (Rinv (g x)))) *)
  intros x [[Hf Hg] H].
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /norm /= /abs /minus /plus /opp /=.
(* Goal: F (fun x : T => P (g x)) *)
  replace (/ g x + - / f x)
(* Goal: F (fun x : T => P (g x)) *)
    with ((f x - g x) / (f x * g x)).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Rabs_div ?Rabs_Rinv ?Rabs_mult //.
(* Goal: Rle (Rdiv (Rabs (Rminus (f x) (g x))) (Rmult (Rabs (f x)) (Rabs (g x)))) (Rmult (pos eps) (Rinv (Rabs (g x)))) *)
(* Goal: not (@eq R (Rmult (f x) (g x)) (IZR Z0)) *)
(* Goal: @eq R (Rdiv (Rminus (f x) (g x)) (Rmult (f x) (g x))) (Rplus (Rinv (g x)) (Ropp (Rinv (f x)))) *)
  apply Rle_div_l.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  apply Rmult_lt_0_compat ; by apply Rabs_pos_lt.
(* Goal: Rle (Rabs (Rminus (f x) (g x))) (Rmult (Rmult (pos eps) (Rinv (Rabs (g x)))) (Rmult (Rabs (f x)) (Rabs (g x)))) *)
(* Goal: not (@eq R (Rmult (f x) (g x)) (IZR Z0)) *)
(* Goal: @eq R (Rdiv (Rminus (f x) (g x)) (Rmult (f x) (g x))) (Rplus (Rinv (g x)) (Ropp (Rinv (f x)))) *)
  field_simplify ; rewrite ?Rdiv_1.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by [].
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rabs_no_R0.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Rmult_integral_contrapositive_currified.
(* Goal: ineqs x *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  field ; by split.
Qed.

(** * Domination and composition *)

Section Domin_comp.

Context {T1 T2 : Type} {Ku Kv : AbsRing}
  {U : NormedModule Ku} {V : NormedModule Kv}
(* Goal: F (fun x : T => P (g x)) *)
  (F : (T1 -> Prop) -> Prop) {FF : Filter F}
(* Goal: F (fun x : T => P (g x)) *)
  (G : (T2 -> Prop) -> Prop) {FG : Filter G}.

(* Goal: F (fun x : T => P (g x)) *)
Lemma domin_comp (f : T2 -> U) (g : T2 -> V) (l : T1 -> T2) :
(* Goal: F (fun x : T => P (g x)) *)
  filterlim l F G -> is_domin G f g
(* Goal: F (fun x : T => P (g x)) *)
    -> is_domin F (fun t => f (l t)) (fun t => g (l t)).
Proof.
(* Goal: forall (_ : @filterlim T1 T2 l F G) (_ : @is_domin T2 Ku Kv U V G f g), @is_domin T1 Ku Kv U V F (fun t : T1 => f (l t)) (fun t : T1 => g (l t)) *)
  intros Hl Hg eps.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  generalize (fun eps => Hl _ (Hg eps)) => {Hl Hg} /= Hl.
(* Goal: F (fun x : T1 => Rle (@norm Kv V (g (l x))) (Rmult (pos eps) (@norm Ku U (f (l x))))) *)
  by apply Hl.
Qed.

End Domin_comp.

(** * Equivalence and limits *)

Lemma filterlim_equiv :
(* Goal: F (fun x : T => P (g x)) *)
  forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> R) (l : Rbar),
(* Goal: F (fun x : T => P (g x)) *)
  is_equiv F f g ->
(* Goal: F (fun x : T => P (g x)) *)
  filterlim f F (Rbar_locally l) ->
  filterlim g F (Rbar_locally l).
Proof.
intros T F FF f g [l| |] Hfg Hf P [eps HP] ;
  apply equiv_sym in Hfg ;
  unfold filtermap.
(* Goal: F (fun x : T => P (g x)) *)
- assert (He: 0 < eps / 2 / (Rabs l + 1)).
(* Goal: Rlt (IZR Z0) (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rdiv_lt_0_compat.
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: Rbar_locally (Finite l) ineqs *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply is_pos_div_2.
(* Goal: Rgt (Rplus (Rabs l) (IZR (Zpos xH))) (IZR Z0) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rplus_le_lt_0_compat.
(* Goal: Rle (IZR Z0) (Rabs l) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rabs_pos.
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_0_1.
(* Goal: F (fun x : T => P (g x)) *)
  pose ineqs (y : R) := Rabs (y - l) < eps/2 /\ Rabs y <= Rabs l + 1.
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  assert (Hl: Rbar_locally l ineqs).
(* Goal: Rbar_locally (Finite l) ineqs *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  assert (H: 0 < Rmin (eps / 2) 1).
(* Goal: Rlt (IZR Z0) (Rmin (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) *)
(* Goal: Rbar_locally (Finite l) ineqs *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rmin_case.
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: Rbar_locally (Finite l) ineqs *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply is_pos_div_2.
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_0_1.
(* Goal: Rbar_locally (Finite l) ineqs *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  exists (mkposreal _ H).
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
  simpl.
(* Goal: forall (y : R) (_ : @ball R_UniformSpace l (Rmin (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) y), ineqs y *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  intros x Hx.
(* Goal: ineqs x *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  split.
(* Goal: Rlt (Rabs (Rminus x l)) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_le_trans with (1 := Hx).
(* Goal: Rle (Rmin (IZR Z0) (Rmult (IZR (Zpos (xO xH))) eps)) (IZR Z0) *)
  apply Rmin_l.
(* Goal: Rle (Rabs x) (Rplus (Rabs l) (IZR (Zpos xH))) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rabs_le_between'.
(* Goal: Rle (Rabs (Rminus (Rabs x) (Rabs l))) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rle_trans with (1 := Rabs_triang_inv2 _ _).
(* Goal: Rle (IZR Z0) (f x) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_le.
(* Goal: Rlt (Rabs (Rminus x l)) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_le_trans with (1 := Hx).
(* Goal: Rle (Rmin (IZR Z0) (Rmult (IZR (Zpos (xO xH))) eps)) (Rmult (IZR (Zpos (xO xH))) eps) *)
(* Goal: Rlt (f x) (IZR Z0) *)
  apply Rmin_r.
  generalize (filter_and  _  (fun (x : T) =>  ineqs (f x))  (Hfg (mkposreal _ He))  (Hf _ Hl)).
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
  apply filter_imp.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
  simpl.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (@norm R_AbsRing R_NormedModule (f x)))) (ineqs (f x))), P (g x) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  intros x [H1 [H2 H3]].
(* Goal: P (g x) *)
  apply HP.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /=.
(* Goal: F (fun x : T => P (g x)) *)
  replace (g x + - l) with ((f x - l) + -(f x - g x)) by ring.
(* Goal: Rlt (Rabs (Rplus (Rminus (f x) l) (Ropp (Rminus (f x) (g x))))) (pos eps) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rle_lt_trans with (1 := Rabs_triang _ _).
(* Goal: Rlt (Rplus (Rabs (Rminus (f x) l)) (Rabs (Ropp (Rminus (f x) (g x))))) (pos eps) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  replace (pos eps) with (eps / 2 + eps / 2 / (Rabs l + 1) * (Rabs l + 1)).
(* Goal: Rlt (Rplus (Rabs (Rminus (f x) l)) (Rabs (Ropp (Rminus (f x) (g x))))) (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (Rplus (Rabs l) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (Rplus (Rabs l) (IZR (Zpos xH))))) (pos eps) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rplus_lt_le_compat with (1 := H2).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Rabs_Ropp.
(* Goal: Rle (Rabs (Rminus (f x) (g x))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) *)
(* Goal: @eq R (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (Rplus (Rabs l) (IZR (Zpos xH))))) (pos eps) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rle_trans with (1 := H1).
(* Goal: Rle (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (@norm R_AbsRing R_NormedModule (f x))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) *)
(* Goal: @eq R (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (Rplus (Rabs l) (IZR (Zpos xH))))) (pos eps) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rmult_le_compat_l with (2 := H3).
(* Goal: Rle (IZR Z0) (f x) *)
(* Goal: F (fun x : T => P (g x)) *)
  now apply Rlt_le.
(* Goal: @eq R (Rplus (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rmult (Rdiv (Rdiv (pos eps) (IZR (Zpos (xO xH)))) (Rplus (Rabs l) (IZR (Zpos xH)))) (Rplus (Rabs l) (IZR (Zpos xH))))) (pos eps) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  field.
(* Goal: not (@eq R (Rplus (Rabs l) (IZR (Zpos xH))) (IZR Z0)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rgt_not_eq.
(* Goal: Rgt (Rplus (Rabs l) (IZR (Zpos xH))) (IZR Z0) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rplus_le_lt_0_compat.
(* Goal: Rle (IZR Z0) (Rabs l) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rabs_pos.
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_0_1.
(* Goal: F (fun x : T => P (g x)) *)
- pose ineq (y : R) := Rmax 0 (2 * eps) < y.
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  assert (Hl: Rbar_locally' p_infty ineq).
(* Goal: Rbar_locally' p_infty ineq *)
(* Goal: F (fun x : T => P (g x)) *)
(* Goal: F (fun x : T => P (g x)) *)
  now exists (Rmax 0 (2 * eps)).
(* Goal: F (fun x : T => P (g x)) *)
  generalize (filter_and _ (fun (x : T) => ineq (f x)) (Hfg (mkposreal _ pos_half_prf)) (Hf _ Hl)).
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
  apply filter_imp.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
  simpl.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (Rinv (IZR (Zpos (xO xH)))) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
  intros x [H1 H2].
(* Goal: P (g x) *)
  apply HP.
(* Goal: Rlt (g x) eps *)
  apply Rabs_le_between' in H1.
(* Goal: F (fun x : T => P (g x)) *)
  generalize (Rplus_le_compat_l (- /2 * Rabs (f x)) _ _ (proj2 H1)).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /norm /= /abs /=.
(* Goal: F (fun x : T => P (g x)) *)
  replace (- / 2 * Rabs (f x) + (g x + / 2 * Rabs (f x))) with (g x) by ring.
(* Goal: forall _ : Rle (Rplus (Rmult (Ropp (Rinv (IZR (Zpos (xO xH))))) (Rabs (f x))) (f x)) (g x), Rlt eps (g x) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_le_trans.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Rabs_pos_eq.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Ropp (f x))) (f x)) eps *)
(* Goal: Rlt (f x) (IZR Z0) *)
  apply Rmult_lt_reg_l with (1 := Rlt_R0_R2).
(* Goal: F (fun x : T => P (g x)) *)
  replace (2 * (- / 2 * f x + f x)) with (f x) by field.
(* Goal: Rlt (IZR Z0) (f x) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rle_lt_trans with (2 := H2).
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) eps) (Rmax (IZR Z0) (Rmult (IZR (Zpos (xO xH))) eps)) *)
(* Goal: Rle (IZR Z0) (f x) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rmax_r.
(* Goal: Rle (IZR Z0) (f x) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rlt_le.
(* Goal: Rlt (IZR Z0) (f x) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rle_lt_trans with (2 := H2).
(* Goal: Rle (IZR Z0) (Rmax (IZR Z0) (Rmult (IZR (Zpos (xO xH))) eps)) *)
(* Goal: F (fun x : T => P (g x)) *)
  apply Rmax_l.
(* Goal: F (fun x : T => P (g x)) *)
- pose ineq (y : R) := y < Rmin 0 (2 * eps).
(* Goal: F (fun x : T => P (g x)) *)
  assert (Hl: Rbar_locally' m_infty ineq).
(* Goal: Rbar_locally' m_infty ineq *)
(* Goal: F (fun x : T => P (g x)) *)
  now exists (Rmin 0 (2 * eps)).
(* Goal: F (fun x : T => P (g x)) *)
  generalize (filter_and _ (fun (x : T) => ineq (f x)) (Hfg (mkposreal _ pos_half_prf)) (Hf _ Hl)).
(* Goal: forall _ : F (fun x : T => and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), F (fun x : T => P (g x)) *)
  apply filter_imp.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (pos (mkposreal (Rinv (IZR (Zpos (xO xH)))) pos_half_prf)) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
  simpl.
(* Goal: forall (x : T) (_ : and (Rle (@norm R_AbsRing R_NormedModule (@minus (NormedModule.AbelianGroup R_AbsRing R_NormedModule) (f x) (g x))) (Rmult (Rinv (IZR (Zpos (xO xH)))) (@norm R_AbsRing R_NormedModule (f x)))) (ineq (f x))), P (g x) *)
  intros x [H1 H2].
(* Goal: P (g x) *)
  apply HP.
(* Goal: Rlt (g x) eps *)
  apply Rabs_le_between' in H1.
(* Goal: Rlt (g x) eps *)
  generalize (Rplus_le_compat_l (/2 * Rabs (f x)) _ _ (proj1 H1)).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite /norm /= /abs /=.
(* Goal: F (fun x : T => P (g x)) *)
  replace (/ 2 * Rabs (f x) + (g x - / 2 * Rabs (f x))) with (g x) by ring.
(* Goal: forall _ : Rle (g x) (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)), Rlt (g x) eps *)
  intros H.
(* Goal: Rlt (g x) eps *)
  apply Rle_lt_trans with (1 := H).
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rabs (f x))) (f x)) eps *)
  rewrite Rabs_left.
(* Goal: Rlt (Rplus (Rmult (Rinv (IZR (Zpos (xO xH)))) (Ropp (f x))) (f x)) eps *)
(* Goal: Rlt (f x) (IZR Z0) *)
  apply Rmult_lt_reg_l with (1 := Rlt_R0_R2).
(* Goal: F (fun x : T => P (g x)) *)
  replace (2 * (/ 2 * - f x + f x)) with (f x) by field.
(* Goal: Rlt (f x) (IZR Z0) *)
  apply Rlt_le_trans with (1 := H2).
(* Goal: Rle (Rmin (IZR Z0) (Rmult (IZR (Zpos (xO xH))) eps)) (Rmult (IZR (Zpos (xO xH))) eps) *)
(* Goal: Rlt (f x) (IZR Z0) *)
  apply Rmin_r.
(* Goal: Rlt (f x) (IZR Z0) *)
  apply Rlt_le_trans with (1 := H2).
(* Goal: Rle (Rmin (IZR Z0) (Rmult (IZR (Zpos (xO xH))) eps)) (IZR Z0) *)
  apply Rmin_l.
Qed.
