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

Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
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 mathcomp.ssreflect.ssreflect.
Require Import Rcomplements Rbar.
Require Import Continuity Derive Hierarchy.

(** This file defines complex numbers [C] as [R * R]. Operations are
given, and [C] is proved to be a field, a normed module, and a
complete space. *)

(** * The set of complex numbers *)

Definition C := (R * R)%type.

Definition RtoC (x : R) : C := (x,0).
Coercion RtoC : R >-> C.

Lemma RtoC_inj : forall (x y : R),
  RtoC x = RtoC y -> x = y.
Proof.
(* Goal: forall (x y : R) (_ : @eq C (RtoC x) (RtoC y)), @eq R x y *)
  intros x y H.
(* Goal: @eq R (Rminus (@fst R R r1) (@fst R R r2)) (IZR Z0) *)
(* Goal: @eq R (Rminus (@snd R R r1) (@snd R R r2)) (IZR Z0) *)
  now apply (f_equal (@fst R R)) in H.
Qed.

Lemma Ceq_dec (z1 z2 : C) : { z1 = z2 } + { z1 <> z2 }.
Proof.
(* Goal: sumbool (@eq C z1 z2) (not (@eq C z1 z2)) *)
  destruct z1 as [x1 y1].
(* Goal: sumbool (@eq C (@pair R R x1 y1) z2) (not (@eq C (@pair R R x1 y1) z2)) *)
  destruct z2 as [x2 y2].
(* Goal: forall _ : @ex_derive C_AbsRing C_NormedModule f z, @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  case: (Req_EM_T x1 x2) => [ -> | Hx ].
(* Goal: forall _ : @ex_derive C_AbsRing C_NormedModule f z, @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  case: (Req_EM_T y1 y2) => [ -> | Hy ].
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by left.
(* Goal: sumbool (@eq C (@pair R R x2 y1) (@pair R R x2 y2)) (not (@eq C (@pair R R x2 y1) (@pair R R x2 y2))) *)
(* Goal: sumbool (@eq C (@pair R R x1 y1) (@pair R R x2 y2)) (not (@eq C (@pair R R x1 y1) (@pair R R x2 y2))) *)
  right ; contradict Hy.
(* Goal: @eq R y1 y2 *)
(* Goal: sumbool (@eq C (@pair R R x1 y1) (@pair R R x2 y2)) (not (@eq C (@pair R R x1 y1) (@pair R R x2 y2))) *)
  now apply (f_equal (@snd R R)) in Hy ; simpl in Hy.
(* Goal: sumbool (@eq C (@pair R R x1 y1) (@pair R R x2 y2)) (not (@eq C (@pair R R x1 y1) (@pair R R x2 y2))) *)
  right ; contradict Hx.
(* Goal: @eq R x1 x2 *)
  now apply (f_equal (@fst R R)) in Hx ; simpl in Hx.
Qed.

(** ** Constants and usual functions *)

(** 0 and 1 for complex are defined as [RtoC 0] and [RtoC 1] *)
Definition Ci : C := (0,1).

(** *** Arithmetic operations *)

Definition Cplus (x y : C) : C := (fst x + fst y, snd x + snd y).
Definition Copp (x : C) : C := (-fst x, -snd x).
Definition Cminus (x y : C) : C := Cplus x (Copp y).
Definition Cmult (x y : C) : C := (fst x * fst y - snd x * snd y, fst x * snd y + snd x * fst y).
Definition Cinv (x : C) : C := (fst x / (fst x ^ 2 + snd x ^ 2), - snd x / (fst x ^ 2 + snd x ^ 2)).
Definition Cdiv (x y : C) : C := Cmult x (Cinv y).

Delimit Scope C_scope with C.
Local Open Scope C_scope.

Infix "+" := Cplus : C_scope.
Notation "- x" := (Copp x) : C_scope.
Infix "-" := Cminus : C_scope.
Infix "*" := Cmult : C_scope.
Notation "/ x" := (Cinv x) : C_scope.
Infix "/" := Cdiv : C_scope.

(** *** Other usual functions *)

Definition Re (z : C) : R := fst z.

Definition Im (z : C) : R := snd z.

Definition Cmod (x : C) : R := sqrt (fst x ^ 2 + snd x ^ 2).

Definition Cconj (x : C) : C := (fst x, (- snd x)%R).

Lemma Cmod_0 : Cmod 0 = 0.
Proof.
(* Goal: @eq R (Cmod (RtoC x)) (Rabs x) *)
unfold Cmod.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
simpl.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Rmult_0_l Rplus_0_l.
(* Goal: @eq R (sqrt (IZR Z0)) (IZR Z0) *)
apply sqrt_0.
Qed.
Lemma Cmod_1 : Cmod 1 = 1.
Proof.
(* Goal: @eq R (Cmod (RtoC x)) (Rabs x) *)
unfold Cmod.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
simpl.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Rmult_0_l Rplus_0_r 2!Rmult_1_l.
(* Goal: @eq R (sqrt (IZR (Zpos xH))) (IZR (Zpos xH)) *)
apply sqrt_1.
Qed.

Lemma Cmod_opp : forall x, Cmod (-x) = Cmod x.
Proof.
(* Goal: @eq R (Cmod (RtoC x)) (Rabs x) *)
unfold Cmod.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
simpl.
(* Goal: forall x : R, @eq R (Cmod (RtoC x)) (Rabs x) *)
intros x.
(* Goal: @eq R (sqrt (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH)))))) (sqrt (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH)))))) *)
apply f_equal.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
ring.
Qed.

Lemma Cmod_triangle : forall x y, Cmod (x + y) <= Cmod x + Cmod y.
Proof.
(* Goal: forall x y : C, Rle (Cmod (Cplus x y)) (Rplus (Cmod x) (Cmod y)) *)
  intros x y ; rewrite /Cmod.
(* Goal: Rle (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y))) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rsqr_incr_0_var.
(* Goal: Rle (Rsqr (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y)))) (Rsqr (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y)))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rminus_le_0.
(* Goal: Rle (IZR Z0) (Rminus (Rsqr (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O))))))) (Rsqr (sqrt (Rplus (pow (@fst R R (Cplus x y)) (S (S O))) (pow (@snd R R (Cplus x y)) (S (S O))))))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  unfold Rsqr ; simpl ; ring_simplify.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite /pow ?Rmult_1_r.
(* Goal: Rle (IZR Z0) (Rminus (Rsqr (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y)))))) (Rsqr (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  rewrite ?sqrt_sqrt ; ring_simplify.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  replace (-2 * fst x * fst y - 2 * snd x * snd y)%R with (- (2 * (fst x * fst y + snd x * snd y)))%R by ring.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Rmult_assoc -sqrt_mult.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Rplus_comm.
(* Goal: Rle (IZR Z0) (Rplus (Rmult (IZR (Zpos (xO xH))) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y)))))) (Ropp (Rmult (IZR (Zpos (xO xH))) (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y)))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply -> Rminus_le_0.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y)))) (Rmult (IZR (Zpos (xO xH))) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y)))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rmult_le_compat_l.
(* Goal: Rle (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: Rle (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y))) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rlt_le, Rlt_0_2.
(* Goal: Rle (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y))) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rsqr_incr_0_var.
(* Goal: Rle (Rsqr (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y)))) (Rsqr (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y)))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rminus_le_0.
(* Goal: Rle (IZR Z0) (Rminus (Rsqr (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y)))))) (Rsqr (Rplus (Rmult (@fst R R x) (@fst R R y)) (Rmult (@snd R R x) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  rewrite /Rsqr ?sqrt_sqrt ; ring_simplify.
  replace (fst x ^ 2 * snd y ^ 2 - 2 * fst x * snd x * fst y * snd y +
    snd x ^ 2 * fst y ^ 2)%R with ( (fst x * snd y - snd x * fst y)^2)%R
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
    by ring.
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply pow2_ge_0.
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  repeat apply Rplus_le_le_0_compat ; apply Rmult_le_pos ; apply pow2_ge_0.
(* Goal: Rle (IZR Z0) (Cmod x) *)
  apply sqrt_pos.
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
  replace (fst x ^ 2 + 2 * fst x * fst y + fst y ^ 2 + snd x ^ 2 + 2 * snd x * snd y + snd y ^ 2)%R
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
    with ((fst x + fst y)^2 + (snd x + snd y)^2)%R by ring.
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
(* Goal: Rle (IZR Z0) (Cmod x) *)
  apply Rplus_le_le_0_compat ; apply sqrt_pos.
Qed.

Lemma Cmod_mult : forall x y, Cmod (x * y) = (Cmod x * Cmod y)%R.
Proof.
(* Goal: forall (x : R) (y : C), @eq (ModuleSpace.sort R_Ring C_R_ModuleSpace) (@scal R_Ring C_R_ModuleSpace x y) (Cmult (RtoC x) y) *)
  intros x y.
(* Goal: @eq R (Cmod (RtoC x)) (Rabs x) *)
  unfold Cmod.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite -sqrt_mult.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply f_equal ; simpl ; ring.
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
Qed.

Lemma Rmax_Cmod : forall x,
  Rmax (Rabs (fst x)) (Rabs (snd x)) <= Cmod x.
Proof.
(* Goal: forall _ : @ex_derive C_AbsRing C_NormedModule f z, @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  case => x y /=.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite -!sqrt_Rsqr_abs.
  apply Rmax_case ; apply sqrt_le_1_alt, Rminus_le_0 ;
(* Goal: Rle (IZR Z0) (pow (Rminus (Rmult (@fst R R x) (@snd R R y)) (Rmult (@snd R R x) (@fst R R y))) (S (S O))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rmult (pow (@fst R R x) (S (S O))) (pow (@fst R R y) (S (S O)))) (Rmult (pow (@fst R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@fst R R y) (S (S O))))) (Rmult (pow (@snd R R x) (S (S O))) (pow (@snd R R y) (S (S O))))) *)
(* Goal: Rle (IZR Z0) (sqrt (Rmult (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R x) (@fst R R x)) (Rmult (@snd R R x) (@snd R R x))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
  rewrite /Rsqr /= ; ring_simplify ; by apply pow2_ge_0.
Qed.
Lemma Cmod_2Rmax : forall x,
  Cmod x <= sqrt 2 * Rmax (Rabs (fst x)) (Rabs (snd x)).
Proof.
  case => x y /= ; apply Rmax_case_strong => H0 ;
  rewrite -!sqrt_Rsqr_abs ;
  rewrite -?sqrt_mult ;
  try (by apply Rle_0_sqr) ;
  try (by apply Rlt_le, Rlt_0_2) ;
  apply sqrt_le_1_alt ; simpl ; [ rewrite Rplus_comm | ] ;
  rewrite /Rsqr ; apply Rle_minus_r ; ring_simplify ;
  apply Rsqr_le_abs_1 in H0 ; by rewrite /pow !Rmult_1_r.
Qed.

(** ** C is a field *)

Lemma RtoC_plus (x y : R) :
  RtoC (x + y) = RtoC x + RtoC y.
Proof.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
  unfold RtoC, Cplus ; simpl.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by rewrite Rplus_0_r.
Qed.
Lemma RtoC_opp (x : R) :
  RtoC (- x) = - RtoC x.
Proof.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
  unfold RtoC, Copp ; simpl.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by rewrite Ropp_0.
Qed.
Lemma RtoC_minus (x y : R) :
  RtoC (x - y) = RtoC x - RtoC y.
Proof.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by rewrite /Cminus -RtoC_opp -RtoC_plus.
Qed.
Lemma RtoC_mult (x y : R) :
  RtoC (x * y) = RtoC x * RtoC y.
Proof.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
  unfold RtoC, Cmult ; simpl.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.
Lemma RtoC_inv (x : R) : (x <> 0)%R -> RtoC (/ x) = / RtoC x.
Proof.
(* Goal: forall _ : not (@eq R x (IZR Z0)), @eq C (RtoC (Rinv x)) (Cinv (RtoC x)) *)
  intros Hx.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply injective_projections ; simpl ; field.
Qed.
Lemma RtoC_div (x y : R) : (y <> 0)%R -> RtoC (x / y) = RtoC x / RtoC y.
Proof.
(* Goal: forall _ : not (@eq R y (IZR Z0)), @eq C (RtoC (Rdiv x y)) (Cdiv (RtoC x) (RtoC y)) *)
  intros Hy.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply injective_projections ; simpl ; field.
Qed.


Lemma Cplus_comm (x y : C) : x + y = y + x.
Proof.
(* Goal: @eq C (Cplus x y) (Cplus y x) *)
  apply injective_projections ; simpl ; apply Rplus_comm.
Qed.
Lemma Cplus_assoc (x y z : C) : x + (y + z) = (x + y) + z.
Proof.
(* Goal: @eq C (Cplus x (Cplus y z)) (Cplus (Cplus x y) z) *)
  apply injective_projections ; simpl ; apply sym_eq, Rplus_assoc.
Qed.
Lemma Cplus_0_r (x : C) : x + 0 = x.
Proof.
(* Goal: @eq C (Cplus x (RtoC (IZR Z0))) x *)
  apply injective_projections ; simpl ; apply Rplus_0_r.
Qed.
Lemma Cplus_0_l (x : C) : 0 + x = x.
Proof.
(* Goal: @eq C (Cplus (RtoC (IZR Z0)) x) x *)
  apply injective_projections ; simpl ; apply Rplus_0_l.
Qed.
Lemma Cplus_opp_r (x : C) : x + -x = 0.
Proof.
(* Goal: @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
  apply injective_projections ; simpl ; apply Rplus_opp_r.
Qed.

Lemma Copp_plus_distr (z1 z2 : C) : - (z1 + z2) = (- z1 + - z2).
Proof.
(* Goal: @eq C (Copp (Cminus z1 z2)) (Cminus z2 z1) *)
  apply injective_projections ; by apply Ropp_plus_distr.
Qed.
Lemma Copp_minus_distr (z1 z2 : C) : - (z1 - z2) = z2 - z1.
Proof.
(* Goal: @eq C (Copp (Cminus z1 z2)) (Cminus z2 z1) *)
  apply injective_projections ; by apply Ropp_minus_distr.
Qed.

Lemma Cmult_comm (x y : C) : x * y = y * x.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.
Lemma Cmult_assoc (x y z : C) : x * (y * z) = (x * y) * z.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.
Lemma Cmult_0_r (x : C) : x * 0 = 0.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.
Lemma Cmult_0_l (x : C) : 0 * x = 0.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.
Lemma Cmult_1_r (x : C) : x * 1 = x.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.
Lemma Cmult_1_l (x : C) : 1 * x = x.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.

Lemma Cinv_r (r : C) : r <> 0 -> r * /r = 1.
Proof.
(* Goal: forall _ : not (@eq C y (RtoC (IZR Z0))), @eq R (Cmod (Cdiv x y)) (Rdiv (Cmod x) (Cmod y)) *)
  move => H.
(* Goal: @eq C (Cmult r (Cinv r)) (RtoC (IZR (Zpos xH))) *)
  apply injective_projections ; simpl ; field.
(* Goal: not (@eq R (Rplus (Rmult (@fst R R r) (@fst R R r)) (Rmult (@snd R R r) (@snd R R r))) (IZR Z0)) *)
  contradict H.
(* Goal: @eq C r (RtoC (IZR Z0)) *)
  apply Rplus_sqr_eq_0 in H.
(* Goal: @eq C r (RtoC (IZR Z0)) *)
  apply injective_projections ; simpl ; by apply H.
(* Goal: not (@eq R (Rplus (Rmult (@fst R R r) (@fst R R r)) (Rmult (@snd R R r) (@snd R R r))) (IZR Z0)) *)
  contradict H.
(* Goal: @eq C r (RtoC (IZR Z0)) *)
  apply Rplus_sqr_eq_0 in H.
(* Goal: @eq C r (RtoC (IZR Z0)) *)
  apply injective_projections ; simpl ; by apply H.
Qed.

Lemma Cinv_l (r : C) : r <> 0 -> /r * r = 1.
Proof.
(* Goal: forall _ : not (@eq C r (RtoC (IZR Z0))), @eq C (Cmult (Cinv r) r) (RtoC (IZR (Zpos xH))) *)
intros Zr.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Cmult_comm.
(* Goal: @eq C (Cmult r (Cinv r)) (RtoC (IZR (Zpos xH))) *)
now apply Cinv_r.
Qed.

Lemma Cmult_plus_distr_l (x y z : C) : x * (y + z) = x * y + x * z.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.

Lemma Cmult_plus_distr_r (x y z : C) : (x + y) * z = x * z + y * z.
Proof.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  apply injective_projections ; simpl ; ring.
Qed.

Definition C_AbelianGroup_mixin :=
  AbelianGroup.Mixin _ _ _ _ Cplus_comm Cplus_assoc Cplus_0_r Cplus_opp_r.

Canonical C_AbelianGroup :=
  AbelianGroup.Pack C C_AbelianGroup_mixin C.

Lemma Copp_0 : Copp 0 = 0.
Proof.
(* Goal: Rlt (@norm R_AbsRing (prod_NormedModule R_AbsRing R_NormedModule R_NormedModule) (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (pos eps)) *)
(* Goal: @eq R (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (sqrt (IZR (Zpos (xO xH)))) *)
  apply: opp_zero.
Qed.

Definition C_Ring_mixin :=
  Ring.Mixin _ _ _ Cmult_assoc Cmult_1_r Cmult_1_l Cmult_plus_distr_r Cmult_plus_distr_l.

Canonical C_Ring :=
  Ring.Pack C (Ring.Class _ _ C_Ring_mixin) C.

Lemma Cmod_m1 :
  Cmod (Copp 1) = 1.
Proof.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Cmod_opp.
(* Goal: @eq R (Cmod (RtoC (IZR (Zpos xH)))) (IZR (Zpos xH)) *)
apply Cmod_1.
Qed.

Lemma Cmod_eq_0 :
  forall x, Cmod x = 0 -> x = 0.
Proof.
intros x H.
unfold Cmod, pow in H.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite 2!Rmult_1_r -sqrt_0 in H.
apply sqrt_inj in H.
(* Goal: @eq C r (RtoC (IZR Z0)) *)
apply Rplus_sqr_eq_0 in H.
now apply injective_projections.
(* Goal: Rle (IZR Z0) (Rplus (Rmult (@fst R R y) (@fst R R y)) (Rmult (@snd R R y) (@snd R R y))) *)
(* Goal: Rle (IZR Z0) (Rplus (Rplus (Rplus (Rplus (Rplus (pow (@fst R R x) (S (S O))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@fst R R x)) (@fst R R y))) (pow (@fst R R y) (S (S O)))) (pow (@snd R R x) (S (S O)))) (Rmult (Rmult (IZR (Zpos (xO xH))) (@snd R R x)) (@snd R R y))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O)))) *)
(* Goal: Rle (IZR Z0) (Rplus (sqrt (Rplus (pow (@fst R R x) (S (S O))) (pow (@snd R R x) (S (S O))))) (sqrt (Rplus (pow (@fst R R y) (S (S O))) (pow (@snd R R y) (S (S O)))))) *)
apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
apply Rle_refl.
Qed.

Definition C_AbsRing_mixin :=
  AbsRing.Mixin _ _ Cmod_0 Cmod_m1 Cmod_triangle (fun x y => Req_le _ _ (Cmod_mult x y)) Cmod_eq_0.

Canonical C_AbsRing :=
  AbsRing.Pack C (AbsRing.Class _ _ C_AbsRing_mixin) C.

Lemma Cmod_ge_0 :
  forall x, 0 <= Cmod x.
Proof.
(* Goal: forall x : R, @eq R (Cmod (RtoC x)) (Rabs x) *)
intros x.
(* Goal: Rle (IZR Z0) (Cmod x) *)
apply sqrt_pos.
Qed.
Lemma Cmod_gt_0 :
  forall (x : C), x <> 0 <-> 0 < Cmod x.
Proof.
(* Goal: forall x : C, iff (not (@eq C x (RtoC (IZR Z0)))) (Rlt (IZR Z0) (Cmod x)) *)
intros x ; split => Hx.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
destruct (Cmod_ge_0 x) => //.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
by apply sym_eq, Cmod_eq_0 in H.
(* Goal: not (@eq C x (RtoC (IZR Z0))) *)
contradict Hx.
(* Goal: not (Rlt (IZR Z0) (Cmod x)) *)
apply Rle_not_lt, Req_le.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
by rewrite Hx Cmod_0.
Qed.

Lemma Cmod_norm :
  forall x : C, Cmod x = (@norm R_AbsRing _ x).
Proof.
(* Goal: forall x : C, @eq R (Cmod x) (@norm R_AbsRing (prod_NormedModule R_AbsRing R_NormedModule R_NormedModule) x) *)
intros [u v].
(* Goal: @eq R (Cmod (RtoC x)) (Rabs x) *)
unfold Cmod.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
simpl.
apply (f_equal2 (fun x y => sqrt (x + y))) ;
  rewrite /norm /= !Rmult_1_r ;
  apply Rsqr_abs.
Qed.

Lemma Cmod_R :
  forall x : R, Cmod x = Rabs x.
Proof.
(* Goal: forall x : R, @eq R (Cmod (RtoC x)) (Rabs x) *)
intros x.
(* Goal: @eq R (Cmod (RtoC x)) (Rabs x) *)
unfold Cmod.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
simpl.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Rmult_0_l Rplus_0_r Rmult_1_r.
(* Goal: @eq R (sqrt (Rmult x x)) (Rabs x) *)
apply sqrt_Rsqr_abs.
Qed.

Lemma Cmod_inv :
  forall x : C, x <> 0 -> Cmod (/ x) = Rinv (Cmod x).
Proof.
(* Goal: forall (x : C) (_ : not (@eq C x (RtoC (IZR Z0)))), @eq R (Cmod (Cinv x)) (Rinv (Cmod x)) *)
intros x Zx.
(* Goal: @eq R (Cmod (Cinv x)) (Rinv (Cmod x)) *)
apply Rmult_eq_reg_l with (Cmod x).
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite -Cmod_mult.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Rinv_r.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Cinv_r.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
rewrite Cmod_R.
(* Goal: @eq R (Rabs (IZR (Zpos xH))) (IZR (Zpos xH)) *)
(* Goal: not (@eq C x (RtoC (IZR Z0))) *)
(* Goal: not (@eq R (Cmod x) (IZR Z0)) *)
(* Goal: not (@eq R (Cmod x) (IZR Z0)) *)
apply Rabs_R1.
(* Goal: not (@eq C x (RtoC (IZR Z0))) *)
(* Goal: not (@eq R (Cmod x) (IZR Z0)) *)
(* Goal: not (@eq R (Cmod x) (IZR Z0)) *)
exact Zx.
(* Goal: not (@eq R (Cmod x) (IZR Z0)) *)
contradict Zx.
(* Goal: @eq C x (RtoC (IZR Z0)) *)
now apply Cmod_eq_0.
(* Goal: not (@eq R (Cmod x) (IZR Z0)) *)
contradict Zx.
(* Goal: @eq C x (RtoC (IZR Z0)) *)
now apply Cmod_eq_0.
Qed.

Lemma Cmod_div (x y : C) : y <> 0 ->
  Cmod (x / y) = Rdiv (Cmod x) (Cmod y).
Proof.
(* Goal: forall _ : not (@eq C y (RtoC (IZR Z0))), @eq R (Cmod (Cdiv x y)) (Rdiv (Cmod x) (Cmod y)) *)
  move => Hy.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite /Cdiv.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Cmod_mult.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by rewrite Cmod_inv.
Qed.

Lemma Cmult_neq_0 (z1 z2 : C) : z1 <> 0 -> z2 <> 0 -> z1 * z2 <> 0.
Proof.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  intros Hz1 Hz2 => Hz.
(* Goal: False *)
  assert (Cmod (z1 * z2) = 0).
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by rewrite Hz Cmod_0.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Cmod_mult in H.
(* Goal: False *)
  apply Rmult_integral in H ; destruct H.
(* Goal: False *)
(* Goal: False *)
  now apply Hz1, Cmod_eq_0.
(* Goal: False *)
  now apply Hz2, Cmod_eq_0.
Qed.

Lemma Cminus_eq_contra : forall r1 r2 : C, r1 <> r2 -> r1 - r2 <> 0.
Proof.
  intros ; contradict H ; apply injective_projections ;
  apply Rminus_diag_uniq.
(* Goal: @eq R (Rminus (@fst R R r1) (@fst R R r2)) (IZR Z0) *)
(* Goal: @eq R (Rminus (@snd R R r1) (@snd R R r2)) (IZR Z0) *)
  now apply (f_equal (@fst R R)) in H.
(* Goal: @eq R (Rminus (@snd R R r1) (@snd R R r2)) (IZR Z0) *)
  now apply (f_equal (@snd R R)) in H.
Qed.

Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.
Proof.
(* Goal: @ring_theory C (RtoC (IZR Z0)) (RtoC (IZR (Zpos xH))) Cplus Cmult Cminus Copp (@eq C) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
constructor.
(* Goal: @ring_theory C (RtoC (IZR Z0)) (RtoC (IZR (Zpos xH))) Cplus Cmult Cminus Copp (@eq C) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
constructor.
(* Goal: forall x : C, @eq C (Cplus (RtoC (IZR Z0)) x) x *)
(* Goal: forall x y : C, @eq C (Cplus x y) (Cplus y x) *)
(* Goal: forall x y z : C, @eq C (Cplus x (Cplus y z)) (Cplus (Cplus x y) z) *)
(* Goal: forall x : C, @eq C (Cmult (RtoC (IZR (Zpos xH))) x) x *)
(* Goal: forall x y : C, @eq C (Cmult x y) (Cmult y x) *)
(* Goal: forall x y z : C, @eq C (Cmult x (Cmult y z)) (Cmult (Cmult x y) z) *)
(* Goal: forall x y z : C, @eq C (Cmult (Cplus x y) z) (Cplus (Cmult x z) (Cmult y z)) *)
(* Goal: forall x y : C, @eq C (Cminus x y) (Cplus x (Copp y)) *)
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cplus_0_l.
(* Goal: forall x y : C, @eq C (Cplus x y) (Cplus y x) *)
(* Goal: forall x y z : C, @eq C (Cplus x (Cplus y z)) (Cplus (Cplus x y) z) *)
(* Goal: forall x : C, @eq C (Cmult (RtoC (IZR (Zpos xH))) x) x *)
(* Goal: forall x y : C, @eq C (Cmult x y) (Cmult y x) *)
(* Goal: forall x y z : C, @eq C (Cmult x (Cmult y z)) (Cmult (Cmult x y) z) *)
(* Goal: forall x y z : C, @eq C (Cmult (Cplus x y) z) (Cplus (Cmult x z) (Cmult y z)) *)
(* Goal: forall x y : C, @eq C (Cminus x y) (Cplus x (Copp y)) *)
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cplus_comm.
(* Goal: forall x y z : C, @eq C (Cplus x (Cplus y z)) (Cplus (Cplus x y) z) *)
(* Goal: forall x : C, @eq C (Cmult (RtoC (IZR (Zpos xH))) x) x *)
(* Goal: forall x y : C, @eq C (Cmult x y) (Cmult y x) *)
(* Goal: forall x y z : C, @eq C (Cmult x (Cmult y z)) (Cmult (Cmult x y) z) *)
(* Goal: forall x y z : C, @eq C (Cmult (Cplus x y) z) (Cplus (Cmult x z) (Cmult y z)) *)
(* Goal: forall x y : C, @eq C (Cminus x y) (Cplus x (Copp y)) *)
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cplus_assoc.
(* Goal: forall x : C, @eq C (Cmult (RtoC (IZR (Zpos xH))) x) x *)
(* Goal: forall x y : C, @eq C (Cmult x y) (Cmult y x) *)
(* Goal: forall x y z : C, @eq C (Cmult x (Cmult y z)) (Cmult (Cmult x y) z) *)
(* Goal: forall x y z : C, @eq C (Cmult (Cplus x y) z) (Cplus (Cmult x z) (Cmult y z)) *)
(* Goal: forall x y : C, @eq C (Cminus x y) (Cplus x (Copp y)) *)
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cmult_1_l.
(* Goal: forall x y : C, @eq C (Cmult x y) (Cmult y x) *)
(* Goal: forall x y z : C, @eq C (Cmult x (Cmult y z)) (Cmult (Cmult x y) z) *)
(* Goal: forall x y z : C, @eq C (Cmult (Cplus x y) z) (Cplus (Cmult x z) (Cmult y z)) *)
(* Goal: forall x y : C, @eq C (Cminus x y) (Cplus x (Copp y)) *)
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cmult_comm.
(* Goal: forall x y z : C, @eq C (Cmult x (Cmult y z)) (Cmult (Cmult x y) z) *)
(* Goal: forall x y z : C, @eq C (Cmult (Cplus x y) z) (Cplus (Cmult x z) (Cmult y z)) *)
(* Goal: forall x y : C, @eq C (Cminus x y) (Cplus x (Copp y)) *)
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cmult_assoc.
(* Goal: forall x y z : C, @eq C (Cmult (Cplus x y) z) (Cplus (Cmult x z) (Cmult y z)) *)
(* Goal: forall x y : C, @eq C (Cminus x y) (Cplus x (Copp y)) *)
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cmult_plus_distr_r.
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
easy.
(* Goal: forall x : C, @eq C (Cplus x (Copp x)) (RtoC (IZR Z0)) *)
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact Cplus_opp_r.
(* Goal: not (@eq C (RtoC (IZR (Zpos xH))) (RtoC (IZR Z0))) *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
intros H.
(* Goal: False *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
injection H.
(* Goal: forall _ : @eq R (IZR (Zpos xH)) (IZR Z0), False *)
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
exact R1_neq_R0.
(* Goal: forall p q : C, @eq C (Cdiv p q) (Cmult p (Cinv q)) *)
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
easy.
(* Goal: forall (p : C) (_ : not (@eq C p (RtoC (IZR Z0)))), @eq C (Cmult (Cinv p) p) (RtoC (IZR (Zpos xH))) *)
apply Cinv_l.
Qed.

Add Field C_field_field : C_field_theory.

(** * C is a NormedModule *)

Canonical C_UniformSpace :=
  UniformSpace.Pack C (UniformSpace.class (prod_UniformSpace _ _)) C.

(** on C (with the balls of R^2) *)

Canonical C_ModuleSpace :=
  ModuleSpace.Pack C_Ring C (ModuleSpace.class _ (Ring_ModuleSpace C_Ring)) C.

Canonical C_NormedModuleAux :=
  NormedModuleAux.Pack C_AbsRing C (NormedModuleAux.Class C_AbsRing _ (ModuleSpace.class _ C_ModuleSpace) (UniformSpace.class C_UniformSpace)) C.

Lemma C_NormedModule_mixin_compat1 :
  forall (x y : C) (eps : R),
  Cmod (minus y x) < eps -> ball x eps y.
Proof.
(* Goal: forall (x y : C) (eps : R) (_ : Rlt (Cmod (@minus C_AbelianGroup y x)) eps), @ball C_UniformSpace x eps y *)
  intros x y eps.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Cmod_norm.
(* Goal: Rlt (@norm R_AbsRing (prod_NormedModule R_AbsRing R_NormedModule R_NormedModule) (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (pos eps)) *)
(* Goal: @eq R (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (sqrt (IZR (Zpos (xO xH)))) *)
  apply: prod_norm_compat1.
Qed.

Lemma C_NormedModule_mixin_compat2 :
  forall (x y : C_NormedModuleAux) (eps : posreal),
  ball x eps y -> Cmod (minus y x) < sqrt 2 * eps.
Proof.
(* Goal: forall (x y : NormedModuleAux.sort C_AbsRing C_NormedModuleAux) (eps : posreal) (_ : @ball (NormedModuleAux.UniformSpace C_AbsRing C_NormedModuleAux) x (pos eps) y), Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  intros x y eps H.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Cmod_norm.
(* Goal: Rlt (@norm R_AbsRing (prod_NormedModule R_AbsRing R_NormedModule R_NormedModule) (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  replace (sqrt 2) with (sqrt 2 * Rmax 1 1)%R.
(* Goal: Rlt (@norm R_AbsRing (prod_NormedModule R_AbsRing R_NormedModule R_NormedModule) (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (pos eps)) *)
(* Goal: @eq R (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (sqrt (IZR (Zpos (xO xH)))) *)
  apply: prod_norm_compat2 H.
  rewrite -> Rmax_left by apply Rle_refl.
(* Goal: @eq R (Rmult (sqrt (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (sqrt (IZR (Zpos (xO xH)))) *)
  apply Rmult_1_r.
Qed.

Definition C_NormedModule_mixin :=
  NormedModule.Mixin _ C_NormedModuleAux _ _ Cmod_triangle (fun x y => Req_le _ _ (Cmod_mult x y))
    C_NormedModule_mixin_compat1 C_NormedModule_mixin_compat2 Cmod_eq_0.

Canonical C_NormedModule :=
  NormedModule.Pack C_AbsRing C (NormedModule.Class _ _ _ C_NormedModule_mixin) C.

(** on R *)

Canonical C_R_ModuleSpace :=
  ModuleSpace.Pack R_Ring C (ModuleSpace.class _ (prod_ModuleSpace R_Ring R_ModuleSpace R_ModuleSpace)) C.

Canonical C_R_NormedModuleAux :=
  NormedModuleAux.Pack R_AbsRing C (NormedModuleAux.Class R_AbsRing _ (ModuleSpace.class _ C_R_ModuleSpace) (UniformSpace.class _)) C.

Canonical C_R_NormedModule :=
  NormedModule.Pack R_AbsRing C (NormedModule.class _ (prod_NormedModule _ _ _)) C.

Lemma scal_R_Cmult :
  forall (x : R) (y : C),
  scal (V := C_R_ModuleSpace) x y = Cmult x y.
Proof.
(* Goal: forall (x : R) (y : C), @eq (ModuleSpace.sort R_Ring C_R_ModuleSpace) (@scal R_Ring C_R_ModuleSpace x y) (Cmult (RtoC x) y) *)
intros x y.
apply injective_projections ;
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  rewrite /scal /= /scal /= /mult /= ; ring.
Qed.

(** * C is a CompleteSpace *)

Definition C_complete_lim (F : (C -> Prop) -> Prop) :=
  (R_complete_lim (fun P => F (fun z => P (Re z))), R_complete_lim (fun P => F (fun z => P (Im z)))).

Lemma C_complete_ax1 :
  forall F : (C -> Prop) -> Prop,
  ProperFilter F ->
  (forall eps : posreal, exists x : C, F (ball x eps)) ->
  forall eps : posreal, F (ball (C_complete_lim F) eps).
Proof.
(* Goal: forall (F : forall _ : forall _ : C, Prop, Prop) (_ : @ProperFilter C F) (_ : forall eps : posreal, @ex C (fun x : C => F (@ball C_UniformSpace x (pos eps)))) (eps : posreal), F (@ball (prod_UniformSpace R_UniformSpace R_UniformSpace) (C_complete_lim F) (pos eps)) *)
  intros.
(* Goal: F (@ball (prod_UniformSpace R_UniformSpace R_UniformSpace) (C_complete_lim F) (pos eps)) *)
  apply filter_and ; simpl ; revert eps.
(* Goal: forall eps : posreal, F (fun x : C => @ball R_UniformSpace (R_complete_lim (fun P : forall _ : R, Prop => F (fun z : C => P (Re z)))) (pos eps) (@fst R R x)) *)
(* Goal: forall eps : posreal, F (fun x : C => @ball R_UniformSpace (R_complete_lim (fun P : forall _ : R, Prop => F (fun z : C => P (Im z)))) (pos eps) (@snd R R x)) *)
  apply (R_complete (fun P => F (fun z => P (Re z)))).
(* Goal: forall (F : forall _ : forall _ : C, Prop, Prop) (_ : @ProperFilter C F) (_ : forall eps : posreal, @ex C (fun x : C => F (@ball C_UniformSpace x (pos eps)))) (eps : posreal), F (@ball (prod_UniformSpace R_UniformSpace R_UniformSpace) (C_complete_lim F) (pos eps)) *)
  split ; intros.
(* Goal: @ex R (fun x : R => P x) *)
(* Goal: @Filter R (fun P : forall _ : R, Prop => F (fun z : C => P (Im z))) *)
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  destruct (filter_ex _ H1).
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by exists (Re x).
(* Goal: @Filter R (fun P : forall _ : R, Prop => F (fun z : C => P (Im z))) *)
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  split.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply filter_true.
(* Goal: forall (x0 : C) (_ : @ball C_UniformSpace x (pos eps) x0), @ball R_UniformSpace (Im x) (pos eps) (Im x0) *)
  intros ; by apply filter_and.
(* Goal: forall (P Q : forall _ : R, Prop) (_ : forall (x : R) (_ : P x), Q x) (_ : F (fun z : C => P (Im z))), F (fun z : C => Q (Im z)) *)
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  intros ; eapply filter_imp, H2.
(* Goal: forall (x0 : C) (_ : @ball C_UniformSpace x (pos eps) x0), @ball R_UniformSpace (Im x) (pos eps) (Im x0) *)
  intros ; by apply H1.
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  intros ; destruct (H0 eps).
(* Goal: @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Re z))) *)
(* Goal: forall eps : posreal, F (fun x : C => @ball R_UniformSpace (R_complete_lim (fun P : forall _ : R, Prop => F (fun z : C => P (Im z)))) (pos eps) (@snd R R x)) *)
  exists (Re x).
(* Goal: F (fun z : C => @ball R_UniformSpace (Im x) (pos eps) (Im z)) *)
  move: H1 ; apply filter_imp.
(* Goal: forall (x0 : C) (_ : @ball C_UniformSpace x (pos eps) x0), @ball R_UniformSpace (Im x) (pos eps) (Im x0) *)
  intros ; by apply H1.
(* Goal: forall eps : posreal, F (fun x : C => @ball R_UniformSpace (R_complete_lim (fun P : forall _ : R, Prop => F (fun z : C => P (Im z)))) (pos eps) (@snd R R x)) *)
  apply (R_complete (fun P => F (fun z => P (Im z)))).
(* Goal: forall (F : forall _ : forall _ : C, Prop, Prop) (_ : @ProperFilter C F) (_ : forall eps : posreal, @ex C (fun x : C => F (@ball C_UniformSpace x (pos eps)))) (eps : posreal), F (@ball (prod_UniformSpace R_UniformSpace R_UniformSpace) (C_complete_lim F) (pos eps)) *)
  split ; intros.
(* Goal: @ex R (fun x : R => P x) *)
(* Goal: @Filter R (fun P : forall _ : R, Prop => F (fun z : C => P (Im z))) *)
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  destruct (filter_ex _ H1).
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by exists (Im x).
(* Goal: @Filter R (fun P : forall _ : R, Prop => F (fun z : C => P (Im z))) *)
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  split.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply filter_true.
(* Goal: forall (x0 : C) (_ : @ball C_UniformSpace x (pos eps) x0), @ball R_UniformSpace (Im x) (pos eps) (Im x0) *)
  intros ; by apply filter_and.
(* Goal: forall (P Q : forall _ : R, Prop) (_ : forall (x : R) (_ : P x), Q x) (_ : F (fun z : C => P (Im z))), F (fun z : C => Q (Im z)) *)
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  intros ; eapply filter_imp, H2.
(* Goal: forall (x0 : C) (_ : @ball C_UniformSpace x (pos eps) x0), @ball R_UniformSpace (Im x) (pos eps) (Im x0) *)
  intros ; by apply H1.
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  intros ; destruct (H0 eps).
(* Goal: @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
  exists (Im x).
(* Goal: F (fun z : C => @ball R_UniformSpace (Im x) (pos eps) (Im z)) *)
  move: H1 ; apply filter_imp.
(* Goal: forall (x0 : C) (_ : @ball C_UniformSpace x (pos eps) x0), @ball R_UniformSpace (Im x) (pos eps) (Im x0) *)
  intros ; by apply H1.
Qed.

Lemma C_complete_ax2 :
  forall F1 F2 : (C -> Prop) -> Prop,
  filter_le F1 F2 ->
  filter_le F2 F1 ->
  close (C_complete_lim F1) (C_complete_lim F2).
Proof.
(* Goal: forall (F1 F2 : forall _ : forall _ : C, Prop, Prop) (_ : @filter_le C F1 F2) (_ : @filter_le C F2 F1), @close (prod_UniformSpace R_UniformSpace R_UniformSpace) (C_complete_lim F1) (C_complete_lim F2) *)
intros F1 F2 H12 H21 eps.
(* Goal: @ball (prod_UniformSpace R_UniformSpace R_UniformSpace) (C_complete_lim F1) (pos eps) (C_complete_lim F2) *)
split ; apply R_complete_close ; intros P.
(* Goal: forall _ : F2 (fun z : C => P (Im z)), F1 (fun z : C => P (Im z)) *)
(* Goal: forall _ : F1 (fun z : C => P (Im z)), F2 (fun z : C => P (Im z)) *)
apply H12.
(* Goal: forall _ : F1 (fun z : C => P (Im z)), F2 (fun z : C => P (Im z)) *)
apply H21.
(* Goal: forall _ : F2 (fun z : C => P (Im z)), F1 (fun z : C => P (Im z)) *)
(* Goal: forall _ : F1 (fun z : C => P (Im z)), F2 (fun z : C => P (Im z)) *)
apply H12.
(* Goal: forall _ : F1 (fun z : C => P (Im z)), F2 (fun z : C => P (Im z)) *)
apply H21.
Qed.

Definition C_CompleteSpace_mixin :=
  CompleteSpace.Mixin _ C_complete_lim C_complete_ax1 C_complete_ax2.

(* on C *)

Canonical C_CompleteNormedModule :=
  CompleteNormedModule.Pack _ C (CompleteNormedModule.Class C_AbsRing _ (NormedModule.class _ C_NormedModule) C_CompleteSpace_mixin) C.

(* on R *)

Canonical C_R_CompleteNormedModule :=
  CompleteNormedModule.Pack _ C (CompleteNormedModule.Class R_AbsRing _ (NormedModule.class _ C_R_NormedModule) C_CompleteSpace_mixin) C.

(** * Locally compat *)

Lemma locally_C x P :
  locally (T := C_UniformSpace) x P <-> locally (T := AbsRing_UniformSpace C_AbsRing) x P.
Proof.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  split => [[e He] | [e He]].
  - exists e => /= y Hy.
    apply He.
(* Goal: @Filter R (fun P : forall _ : R, Prop => F (fun z : C => P (Im z))) *)
(* Goal: forall eps : posreal, @ex R (fun x : R => F (fun z : C => @ball R_UniformSpace x (pos eps) (Im z))) *)
    split.
    eapply Rle_lt_trans, Hy.
    eapply Rle_trans, Rmax_Cmod.
    apply Rmax_l.
    eapply Rle_lt_trans, Hy.
    eapply Rle_trans, Rmax_Cmod.
    apply Rmax_r.
  - assert (Hd : 0 < e / sqrt 2).
    apply Rdiv_lt_0_compat.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
    by apply e.
    apply Rlt_sqrt2_0.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
    exists (mkposreal _ Hd) => /= y [Hy1 Hy2].
    apply He.
    eapply Rle_lt_trans.
    apply Cmod_2Rmax.
    rewrite Rmult_comm ; apply Rlt_div_r.
    apply Rlt_sqrt2_0.
    apply Rmax_case.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
    by apply Hy1.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
    by apply Hy2.
Qed.

(** * Limits *)

Definition C_lim (f : C -> C) (z : C) : C :=
  (real (Lim (fun x => fst (f (x, snd z))) (fst z)),
  real (Lim (fun x => snd (f (x, snd z))) (fst z))).

Lemma is_C_lim_unique (f : C -> C) (z l : C) :
  filterlim f (locally' z) (locally l) -> C_lim f z = l.
Proof.
(* Goal: forall _ : @ex_derive C_AbsRing C_NormedModule f z, @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  case: l => lx ly H.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
  apply injective_projections ; simpl.

(* Goal: @eq R (real (Lim (fun x : R => @fst R R (f (@pair R R x (@snd R R z)))) (Finite (@fst R R z)))) lx *)
(* Goal: @eq R (real (Lim (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Finite (@fst R R z)))) ly *)
  apply (f_equal real (y := Finite lx)).
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  apply is_lim_unique => /= P [eps Hp].
(* Goal: @filtermap R R (fun x : R => @fst R R (f (@pair R R x (@snd R R z)))) (Rbar_locally' (Finite (@fst R R z))) P *)
(* Goal: @eq R (real (Lim (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Finite (@fst R R z)))) ly *)
  destruct (H (fun z => P (fst z))) as [delta Hd] ; clear H.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  exists eps => y Hy.
(* Goal: P (@fst R R y) *)
(* Goal: @filtermap R R (fun x : R => @fst R R (f (@pair R R x (@snd R R z)))) (Rbar_locally' (Finite (@fst R R z))) P *)
(* Goal: @eq R (real (Lim (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Finite (@fst R R z)))) ly *)
  apply Hp, Hy.
(* Goal: @filtermap R R (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Rbar_locally' (Finite (@fst R R z))) P *)
  exists delta.
(* Goal: forall (y : UniformSpace.sort R_UniformSpace) (_ : @ball R_UniformSpace (@fst R R z) (pos delta) y) (_ : not (@eq (UniformSpace.sort R_UniformSpace) y (@fst R R z))), P (@snd R R (f (@pair R R y (@snd R R z)))) *)
  intros y By Hy.
(* Goal: P (@snd R R (f (@pair R R y (@snd R R z)))) *)
  apply Hd.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
  split ; simpl.
(* Goal: @ball R_UniformSpace (@fst R R z) (pos delta) y *)
(* Goal: @ball R_UniformSpace (@snd R R z) (pos delta) (@snd R R z) *)
(* Goal: not (@eq (UniformSpace.sort C_UniformSpace) (@pair R R y (@snd R R z)) z) *)
  apply By.
(* Goal: @ball R_UniformSpace (@snd R R z) (pos delta) (@snd R R z) *)
(* Goal: not (@eq (UniformSpace.sort C_UniformSpace) (@pair R R y (@snd R R z)) z) *)
  apply ball_center.
(* Goal: not (@eq (UniformSpace.sort C_UniformSpace) (@pair R R y (@snd R R z)) z) *)
  contradict Hy.
  clear -Hy.
(* Goal: @eq (UniformSpace.sort R_UniformSpace) y (@fst R R z) *)
  destruct z as [z1 z2].
(* Goal: @eq (UniformSpace.sort R_UniformSpace) y (@fst R R (@pair R R z1 z2)) *)
  now injection Hy.

(* Goal: @eq R (real (Lim (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Finite (@fst R R z)))) ly *)
  apply (f_equal real (y := Finite ly)).
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  apply is_lim_unique => /= P [eps Hp].
(* Goal: @filtermap R R (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Rbar_locally' (Finite (@fst R R z))) P *)
  destruct (H (fun z => P (snd z))) as [delta Hd] ; clear H.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  exists eps => y Hy.
(* Goal: P (@snd R R y) *)
(* Goal: @filtermap R R (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Rbar_locally' (Finite (@fst R R z))) P *)
  apply Hp.
(* Goal: @ball R_UniformSpace ly (pos eps) (@snd R R y) *)
(* Goal: @filtermap R R (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Rbar_locally' (Finite (@fst R R z))) P *)
  apply Hy.
(* Goal: @filtermap R R (fun x : R => @snd R R (f (@pair R R x (@snd R R z)))) (Rbar_locally' (Finite (@fst R R z))) P *)
  exists delta.
(* Goal: forall (y : UniformSpace.sort R_UniformSpace) (_ : @ball R_UniformSpace (@fst R R z) (pos delta) y) (_ : not (@eq (UniformSpace.sort R_UniformSpace) y (@fst R R z))), P (@snd R R (f (@pair R R y (@snd R R z)))) *)
  intros y By Hy.
(* Goal: P (@snd R R (f (@pair R R y (@snd R R z)))) *)
  apply Hd.
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
  split ; simpl.
(* Goal: @ball R_UniformSpace (@fst R R z) (pos delta) y *)
(* Goal: @ball R_UniformSpace (@snd R R z) (pos delta) (@snd R R z) *)
(* Goal: not (@eq (UniformSpace.sort C_UniformSpace) (@pair R R y (@snd R R z)) z) *)
  apply By.
(* Goal: @ball R_UniformSpace (@snd R R z) (pos delta) (@snd R R z) *)
(* Goal: not (@eq (UniformSpace.sort C_UniformSpace) (@pair R R y (@snd R R z)) z) *)
  apply ball_center.
(* Goal: not (@eq (UniformSpace.sort C_UniformSpace) (@pair R R y (@snd R R z)) z) *)
  contradict Hy.
  clear -Hy.
(* Goal: @eq (UniformSpace.sort R_UniformSpace) y (@fst R R z) *)
  destruct z as [z1 z2].
(* Goal: @eq (UniformSpace.sort R_UniformSpace) y (@fst R R (@pair R R z1 z2)) *)
  now injection Hy.
Qed.

(** * Derivatives *)

Definition C_derive (f : C -> C) (z : C) := C_lim (fun x => (f x - f z) / (x - z)) z.

Lemma is_C_derive_unique (f : C -> C) (z l : C) :
  is_derive f z l -> C_derive f z = l.
Proof.
  intros [_ Df].
  specialize (Df _ (fun P H => H)).
  apply is_C_lim_unique.
  intros P HP.
  destruct HP as [eps HP].
  destruct (Df (pos_div_2 eps)) as [eps' Df'].
  unfold filtermap, locally', within.

  apply locally_C.
  exists eps'.
  intros y Hy Hyz.
  apply HP.
  assert (y - z <> 0).
  contradict Hyz.
(* Goal: @eq R (Rplus (Rmult (Ropp (@fst R R x)) (Rmult (Ropp (@fst R R x)) (IZR (Zpos xH)))) (Rmult (Ropp (@snd R R x)) (Rmult (Ropp (@snd R R x)) (IZR (Zpos xH))))) (Rplus (Rmult (@fst R R x) (Rmult (@fst R R x) (IZR (Zpos xH)))) (Rmult (@snd R R x) (Rmult (@snd R R x) (IZR (Zpos xH))))) *)
  replace y with (y - z + z) by ring.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Hyz.
  apply Cplus_0_l.
(* Goal: Rlt (@norm R_AbsRing (prod_NormedModule R_AbsRing R_NormedModule R_NormedModule) (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (pos eps)) *)
(* Goal: @eq R (Rmult (sqrt (IZR (Zpos (xO xH)))) (Rmax (IZR (Zpos xH)) (IZR (Zpos xH)))) (sqrt (IZR (Zpos (xO xH)))) *)
  apply: norm_compat1.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite /minus /plus /opp /=.
  replace ((f y - f z) / (y - z) + - l) with
    ((f y + - f z + - ((y + - z) * l)) / (y + - z)).
  2: by field.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  rewrite /norm /= Cmod_div => //.
  apply Rlt_div_l.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply Cmod_gt_0.
  eapply Rle_lt_trans.
  apply (Df' y Hy).
(* Goal: @eq R (sqrt (Rplus (pow (@fst R R (RtoC x)) (S (S O))) (pow (@snd R R (RtoC x)) (S (S O))))) (Rabs x) *)
  simpl.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite /Rdiv Rmult_assoc.
  apply Rmult_lt_compat_l.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply eps.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite Rmult_comm Rlt_div_l.
(* Goal: Rlt (Cmod (@minus (NormedModuleAux.AbelianGroup C_AbsRing C_NormedModuleAux) y x)) (Rmult (sqrt (IZR (Zpos (xO xH)))) (pos eps)) *)
  rewrite /norm /minus /plus /opp /= /abs /=.
  apply Rminus_lt_0 ; ring_simplify.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply Cmod_gt_0.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply Rlt_0_2.
Qed.
Lemma C_derive_correct (f : C -> C) (z l : C) :
  ex_derive f z -> is_derive f z (C_derive f z).
Proof.
(* Goal: forall _ : @ex_derive C_AbsRing C_NormedModule f z, @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  case => df Hf.
(* Goal: @is_derive C_AbsRing C_NormedModule f z (C_derive f z) *)
  replace (C_derive f z) with df => //.
(* Goal: @eq (NormedModule.sort C_AbsRing C_NormedModule) df (C_derive f z) *)
  by apply sym_eq, is_C_derive_unique.
Qed.

