# Library Coqtail.Complex.Cprop_base

Require Import Ctacfield.
Require Import Cbase.
Require Import Cpow.

# Decidability lemmas

Lemma Ceq_dec : z1 z2 : C, {z1 = z2} + {z1 z2}.
Proof.
intros z1 z2 ; destruct z1 as (r1, r2) ; destruct z2 as (r3, r4).
destruct Req_or_neq with (r1- r3)%R; destruct Req_or_neq with (r2 - r4)%R.
left; CusingR.
right ; intro Habs ; apply Ceq in Habs ; destruct Habs ; auto with real.
right ; intro Habs ; apply Ceq in Habs ; destruct Habs ; auto with real.
right ; intro Habs ; apply Ceq in Habs ; destruct Habs ; auto with real.
Qed.

Lemma Ceq_or_neq_C0 : z, {z = 0} + {z 0}.
Proof.
intro z ; apply Ceq_dec.
Qed.

# Good relations on Cre Cim

Lemma Cre_mult_compat_l : (a:R) (b:C), (Cre (a × b) = a × Cre b)%R.
Proof.
intros a b.
CusingR_rec.
simpl ; field.
Qed.

Lemma Cre_mult_compat_r : (a:C) (b:R), (Cre (a × b) = (Cre a) × b)%R.
Proof.
intros a b.
CusingR_rec.
simpl ; field.
Qed.

Lemma Cim_mult_compat_l : (a:R) (b:C), (Cim (a × b) = a × Cim b)%R.
Proof.
intros a b.
CusingR_rec.
simpl ; field.
Qed.

Lemma Cim_mult_compat_r : (a:C) (b:R), (Cim (a × b) = (Cim a) × b)%R.
Proof.
intros a b.
CusingR_rec.
simpl ; field.
Qed.

Lemma Cre_add_distr : a b : C, Cre (a + b) = (Cre a + Cre b)%R .
Proof.
intros a b.
CusingR_rec; simpl.
reflexivity.
Qed.

Lemma Cim_add_distr : a b : C, Cim (a + b) = (Cim a + Cim b)%R .
Proof.
intros a b.
CusingR_rec; simpl.
reflexivity.
Qed.

### Compatibility of functions with equalities (Hint database)

Lemma Ceq_dec_prop : z1 z2 : C, z1 = z2 z1 z2.
Proof.
intros z1 z2 ; case (Ceq_dec z1 z2) ; intro H ; [left | right] ; assumption.
Qed.
Hint Resolve Ceq_dec_prop: complex.

# IRC

Lemma eq_IRC_compat : (r r' : R), IRC r = IRC r' → (r = r')%R.
Proof.
intros r r' T ; destruct (proj2 (Ceq _ _) T) as [H _] ; assumption.
Qed.

Lemma IRC_eq_compat : (r r' : R), (r = r')%Rr = r'.
Proof.
intros ; subst ; reflexivity.
Qed.
Hint Resolve IRC_eq_compat: complex.

Lemma Cadd_ne : z, z + 0 = z 0 + z = z.
Proof.
intros.
split ; reflexivity.
Qed.

Hint Resolve (f_equal (A:=C)): complex.

Lemma Cadd_eq_compat_l : z z1 z2, z1 = z2z + z1 = z + z2.
Proof.
intros; subst; trivial.
Qed.

Lemma Cadd_eq_compat_r : z z1 z2, z1 = z2z1 + z = z2 + z.
Proof.
intros; subst; trivial.
Qed.

Lemma Cadd_eq_compat a b c d : a = cb = da + b = c + d.
Proof.
intros; subst; trivial.
Qed.

Lemma Cadd_eq_reg_l : z z1 z2, z + z1 = z + z2z1 = z2.
Proof.
intros z z1 z2 H.
destruct z as (r, r0) ; destruct z1 as (r1, r2) ; destruct z2 as (r3, r4).
simpl in ×.
apply ( (Ceq _ _)) in H. destruct H. simpl in ×.
apply Rplus_eq_reg_l in H. apply Rplus_eq_reg_l in H0.
rewrite H; rewrite H0.
reflexivity.
Qed.

Lemma Cadd_eq_reg_r : z z1 z2, z1 + z = z2 + zz1 = z2.
Proof.
intros z z1 z2 H.
rewrite H.
Qed.

# Multiplication

Lemma Cmult_0_r : z, z × 0 = 0.
Proof.
CusingR_f.
Qed.
Hint Resolve Cmult_0_r: complex.

Lemma Cmult_0_l : z, 0 × z = 0.
Proof.
intro.
rewrite Cmult_comm; apply Cmult_0_r.
Qed.
Hint Resolve Cmult_0_l: complex.

Lemma Cmult_eq_compat_l : z z1 z2 : C, z1 = z2z × z1 = z × z2.
Proof.
intros z z1 z2 H.
rewrite H ; reflexivity.
Qed.
Hint Resolve Cmult_eq_compat_l : complex.

Lemma Cmult_eq_compat_r : z z1 z2 : C, z1 = z2z1 × z = z2 × z.
Proof.
intros z z1 z2 H.
rewrite H ; reflexivity.
Qed.
Hint Resolve Cmult_eq_compat_r : complex.

Lemma Cmult_eq_reg_l : z z1 z2 : C, z 0 → z × z1 = z × z2z1 = z2.
Proof.
intros z z1 z2 H0 H.
assert (H1 : (/ z × z × z1 = z1)).
rewrite Cinv_l . apply Cmult_1_l . exact H0.
assert (H2 : (/ z × z × z2 = z2)).
rewrite Cinv_l . apply Cmult_1_l . exact H0.
rewrite <- H1.
rewrite Cmult_assoc. rewrite H.
rewrite <- Cmult_assoc; apply H2.
Qed.

Lemma Cmult_eq_reg_r : z z1 z2 : C, z 0 → z1 × z = z2 × zz1 = z2.
Proof.
intros z z1 z2 H H1.
apply Cmult_eq_reg_l with z.
exact H.
rewrite Cmult_comm ; rewrite H1 ; apply Cmult_comm.
Qed.

Lemma Cmult_integral : z1 z2, z1 × z2 = 0 → z1 = 0 z2 = 0.
Proof.
intros z1 z2 H.
elim (Ceq_dec z1 0) ; elim (Ceq_dec z2 0) ; intros H2 H1.
left ; exact H1.
left ; exact H1.
right ; exact H2.
rewrite <- (Cmult_0_r z1) in H ; apply Cmult_eq_reg_l in H.
right ; assumption.
assumption.
Qed.

Lemma Cmult_eq_0_compat : z1 z2 : C, z1 = 0 z2 = 0 → z1 × z2 = 0.
Proof.
intros z1 z2 H; elim H ; intros H1.
rewrite H1 ; rewrite Cmult_0_l ; reflexivity.
rewrite H1 ; rewrite Cmult_0_r ; reflexivity.
Qed.
Hint Resolve Cmult_eq_0_compat: complex.

Lemma Cmult_eq_0_compat_r : z1 z2 : C, z1 = 0 → z1 × z2 = 0.
Proof.
auto with complex.
Qed.

Lemma Cmult_eq_0_compat_l : z1 z2 : C, z2 = 0 → z1 × z2 = 0.
Proof.
auto with complex.
Qed.

Lemma Cmult_neq_0_reg : z1 z2 : C, z1 × z2 0 → z1 0 z2 0.
Proof.
auto 6 with complex.
Qed.

Lemma Cmult_integral_contrapositive :
z1 z2 : C, z1 0 z2 0 → z1 × z2 0.
Proof.
intros z1 z2 H.
destruct H as (H1, H2).
intro H ; apply H1 ; apply Cmult_integral in H ; elim H ; intro Hdet.
exact Hdet.
rewrite Hdet in H2 ; destruct H2 ; reflexivity.
Qed.
Hint Resolve Cmult_integral_contrapositive: complex.

Lemma Cmult_integral_contrapositive_currified :
z1 z2 : C, z1 0 → z2 0 → z1 × z2 0.
Proof.
auto with complex.
Qed.

# Opposite

Lemma Copp_eq_compat : z1 z2 : C, z1 = z2- z1 = - z2.
Proof.
auto with complex.
Qed.
Hint Resolve Copp_eq_compat: complex.

Lemma Copp_0 : -0 = 0.
Proof.
rewrite <- Ceq ; simpl ; rewrite Ropp_0 ; split ; trivial.
Qed.
Hint Resolve Copp_0: complex.

Lemma Copp_eq_0_compat : z : C, z = 0 → - z = 0.
Proof.
intros z H; rewrite H ; apply Copp_0.
Qed.
Hint Resolve Copp_eq_0_compat: complex.

Lemma Copp_involutive : z : C, - - z = z.
Proof.
CusingR.
Qed.
Hint Resolve Copp_involutive: complex.

Lemma Copp_neq_0_compat : z : C, z 0 → - z 0.
Proof.
intros z H Habs.
apply Copp_eq_0_compat in Habs.
rewrite Copp_involutive in Habs.
apply H ; assumption.
Qed.
Hint Resolve Copp_neq_0_compat: complex.

Lemma Copp_add_distr : z1 z2 : C, - (z1 + z2) = - z1 + - z2.
Proof.
CusingR.
Qed.

# Opposite and multiplication

Lemma Cmult_opp_1_opp : z, -1 × z = -z.
Proof.
intro z ; CusingR_f.
Qed.
Hint Resolve Cmult_opp_1_opp: complex.

Lemma Copp_mult_distr_l_reverse : z1 z2 : C, - z1 × z2 = - (z1 × z2).
Proof.
CusingR_f.
Qed.
Hint Resolve Copp_mult_distr_l_reverse: complex.

Lemma Cmult_opp_opp : z1 z2 : C, - z1 × - z2 = z1 × z2.
Proof.
CusingR_f.
Qed.
Hint Resolve Cmult_opp_opp: complex.

Lemma Copp_mult_distr_r_reverse : z1 z2 : C, z1 × - z2 = - (z1 × z2).
Proof.
CusingR_f.
Qed.

# Minus

Lemma Cminus_0_r : z : C, z - 0 = z.
Proof.
CusingR_f.
Qed.
Hint Resolve Cminus_0_r: complex.

Lemma Cminus_0_l : z : C, 0 - z = - z.
Proof.
CusingR.
Qed.
Hint Resolve Cminus_0_l : complex.

Lemma Copp_minus_distr : z1 z2 : C, - (z1 - z2) = z2 - z1.
Proof.
CusingR_f.
Qed.
Hint Resolve Copp_minus_distr: complex.

Lemma Copp_minus_distr' : z1 z2 : C, - (z2 - z1) = z1 - z2.
Proof.
CusingR_f.
Qed.

Lemma Cminus_diag_eq : z1 z2 : C, z1 = z2z1 - z2 = 0.
Proof.
intros z1 z2 H ; destruct H ; CusingR.
Qed.
Hint Resolve Cminus_diag_eq: complex.

Lemma Cminus_diag_uniq : z1 z2 : C, z1 - z2 = 0 → z1 = z2.
Proof.
intros z1 z2 H.
destruct z1 as (r, r0) ; destruct z2 as (r1, r2) ; rewrite <-Ceq in H ; rewrite <-Ceq ; simpl in ×.
elim H ; intro H1 ; split ; apply Rminus_diag_uniq ; assumption.
Qed.
Hint Immediate Cminus_diag_uniq: complex.

Lemma Cminus_diag_uniq_sym : z1 z2 : C, z2 - z1 = 0 → z1 = z2.
Proof.
intros ; apply Cminus_diag_uniq.
apply Cminus_diag_uniq in H.
rewrite H ; auto with complex.
Qed.
Hint Immediate Cminus_diag_uniq_sym: complex.

Lemma Cadd_minus : z1 z2 : C, z1 + (z2 - z1) = z2.
Proof.
CusingR_f.
Qed.

Lemma Cminus_eq_contra : z1 z2 : C, z1 z2z1 - z2 0.
Proof.
intros z1 z2 H Habs.
apply Cminus_diag_uniq in Habs.
rewrite Habs in H.
apply H ; reflexivity.
Qed.
Hint Resolve Cminus_eq_contra: complex.

Lemma Cminus_not_eq : z1 z2 : C, z1 - z2 0 → z1 z2.
Proof.
intros z1 z2 H Habs.
rewrite Habs in H ; apply H ; auto with complex.
Qed.
Hint Resolve Cminus_not_eq: complex.

Lemma Cminus_not_eq_right : z1 z2 : C, z2 - z1 0 → z1 z2.
Proof.
auto with complex.
Qed.
Hint Resolve Cminus_not_eq_right: complex.

Lemma Cmult_minus_distr_l : z1 z2 z3 : C, z1 × (z2 - z3) = z1 × z2 - z1 × z3.
Proof.
CusingR_f.
Qed.

Lemma Cmult_minus_distr_r : z1 z2 z3 : C, (z2 - z3) × z1 = z2 × z1 - z3 × z1.
Proof.
intros ; rewrite Cmult_comm, Cmult_minus_distr_l ; ring.
Qed.

# Inversion

Lemma Cinv_1 : /1 = 1.
Proof.
field.
auto with complex.
Qed.

Lemma Cinv_R1 : /R1 = 1.
Proof.
CusingR_f.
Qed.

Lemma Cinv_neq_0_compat : z : C, z 0 → / z 0.
Proof.
intros z H.
intro H0.
apply (Cmult_eq_0_compat_l z) in H0.
apply Cinv_r in H.
rewrite H in H0.
apply C1_neq_C0 ; exact H0.
Qed.
Hint Resolve Cinv_neq_0_compat: complex.

Lemma Cinv_involutive : z : C, z 0 → / / z = z.
Proof.
intros z H ; field ; auto with complex.
Qed.
Hint Resolve Cinv_involutive: complex.

Lemma Cinv_mult_distr :
z1 z2 : C, z1 0 → z2 0 → / (z1 × z2) = / z1 × / z2.
Proof.
intros z1 z2 H1 H2 ; field ; split ; assumption.
Qed.

Lemma Copp_inv_permute : z : C, z 0 → - / z = / - z.
Proof.
intros z H ; field ; auto with complex.
Qed.

Lemma Cinv_r_simpl_r : z1 z2 : C, z1 0 → z1 × / z1 × z2 = z2.
Proof.
intros z1 z2 H ; field ; assumption.
Qed.
Hint Resolve Cinv_r_simpl_r : complex.

Lemma Cinv_r_simpl_l : z1 z2 : C, z1 0 → z2 × z1 × / z1 = z2.
Proof.
intros z1 z2 H ; field ; assumption.
Qed.
Hint Resolve Cinv_r_simpl_l : complex.

Lemma Cinv_r_simpl_m : z1 z2 : C, z1 0 → z1 × z2 × / z1 = z2.
Proof.
intros z1 z2 H ; field ; assumption.
Qed.
Hint Resolve Cinv_r_simpl_m: complex.

Lemma Cinv_mult_simpl :
z1 z2 z3 : C, z1 0 → z1 × / z2 × (z3 × / z1) = z3 × / z2.
Proof.
intros z1 z2 z3 H.
rewrite Cmult_assoc ; rewrite Cmult_comm ; rewrite Cmult_assoc.
replace (z3 × /z1 × z1) with z3 by (field ; assumption).
apply Cmult_comm.
Qed.

Lemma Cpow_inv : z n, z 0 → /(z ^ n) = (/z) ^ n.
Proof.
intros z n z_neq ; induction n.
repeat (rewrite Cpow_0) ; CusingR_f.
simpl ; rewrite Cinv_mult_distr ; [| assumption |].
rewrite <- IHn ; reflexivity.
clear -z_neq ; induction n.
simpl ; intuition.
simpl ; apply Cmult_integral_contrapositive ; split ; assumption.
Qed.

# Power

Lemma Cpow_neq_compat : z n, z 0 → z ^ n 0.
Proof.
intros z n z_neq ; induction n.
simpl ; auto with complex.
simpl ; apply Cmult_integral_contrapositive_currified ; assumption.
Qed.

# Injection from R to C

Lemma IRC_minus_compat : lb ub, IRC lb - IRC ub = IRC (lb - ub).
Proof.
intros ; CusingR.
Qed.

Lemma IRC_neq_compat : r s, r sIRC r IRC s.
Proof.
intros r s r_neq_s Hf.
destruct (proj2 (Ceq _ _) Hf) as [Hf' _].
simpl in Hf' ; intuition.
Qed.

Lemma IRC_neq_0_compat : r:R, r 0%RIRC r 0.
Proof.
intros r r_neq_0 ; replace 0 with (IRC 0%R) by intuition ;
apply IRC_neq_compat ; assumption.
Qed.

# Injection from N to C

Lemma S_INC : n:nat, INC (S n) = INC n + 1.
Proof.
intro n . simpl. destruct n ; auto with complex.
Qed.

Lemma IRC_INR_INC : x, IRC (INR x) = INC x.
Proof.
intros x.
induction x. reflexivity.
rewrite S_INC. rewrite <- IHx.
rewrite S_INR. CusingR.
Qed.

Lemma S_O_add_INC : n:nat, INC (1 + n) = INC 1 + INC n.
Proof.
destruct n . auto with complex.
replace (1 + S n)%nat with (S (S n))%nat by (simpl ; reflexivity).
do 3 (rewrite S_INC) ; replace (INC 0%nat) with 0 by (simpl ; reflexivity).
ring.
Qed.

Lemma add_INC : n m:nat, INC (n + m) = INC n + INC m.
Proof.
intros n m.
induction n ; auto with complex.
rewrite Cadd_comm in IHn ; rewrite <- IHn.
replace (S n + m)%nat with (S (n + m)) by (simpl ; reflexivity).
rewrite S_INC ; auto with complex.
Qed.

Lemma minus_INC : n m:nat, (m n)%natINC (n - m) = INC n - INC m.
Proof.
intros n m H1.
induction m.
simpl.
replace (n-0)%nat with n by intuition ; auto with complex.
destruct n.
inversion H1.
replace (S n - S m)%nat with (n - m)%nat by intuition.
do 2 rewrite S_INC. replace (INC n + 1 - (INC m + 1)) with (INC n - INC m) by ring.
replace (INC (S n) - INC m) with (1 + INC n - INC m) in IHm.
replace (INC (S n - m)) with (1 + INC (n - m)) in IHm.
assert ( H :( 1 + INC (n - m) = 1 + INC n - INC m) → (INC (n - m) = INC n - INC m)).
apply H. apply IHm. intuition.
replace (S n - m)%nat with (S (n - m))%nat.
rewrite S_INC. auto with complex.
intuition.
rewrite S_INC. ring.
Qed.
Hint Resolve minus_INC : complex.

Lemma mult_INC : n m:nat, INC (n × m) = INC n × INC m.
Proof.
intros n m; induction n.
intuition.
rewrite S_INC. simpl (S n × m)%nat. rewrite add_INC.
rewrite IHn.
ring.
Qed.
Hint Resolve mult_INC: complex.

Lemma Cre_INC_pos : n : nat, 0 Cre (INC n).
Proof.
induction n.
intuition.
rewrite S_INC.
destruct (INC n); simpl in ×.
intuition.
Qed.

Lemma Cim_INC_0 : n : nat, R0 = Cim (INC n).
Proof.
induction n. intuition.
rewrite S_INC.
rewrite <- IHn.
intuition.
Qed.

# Cnorm

Lemma Cnorm_eq_compat : z z', z = z'Cnorm z = Cnorm z'.
Proof.
intros ; subst ; reflexivity.
Qed.
Hint Resolve Cnorm_eq_compat: complex.

Lemma Cnorm_sqr_pos : r r1 : R, 0 r × r + r1 × r1.
Proof.
intros. apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
Qed.

Lemma Cnorm_sqr_pos_lt : r r1 : R, (r,r1) 0 → 0 < r × r + r1 × r1.
Proof.
intros r r1 z_neq_0.
case (proj1 (C0_neq_R0_neq _) z_neq_0) ; simpl ; intro H.
apply Rplus_lt_le_0_compat.
apply Rsqr_pos_lt ; assumption.
apply Rle_0_sqr.
apply Rplus_le_lt_0_compat.
apply Rle_0_sqr.
apply Rsqr_pos_lt ; assumption.
Qed.

Lemma Cnorm_lt_INC : n m:nat, (n < m)%natCnorm (INC n) < Cnorm (INC m).
Proof.
intros n m H. induction H.
generalize (Cre_INC_pos n). generalize (Cim_INC_0 n).
intros H1 H2.
rewrite S_INC.
destruct (INC n).
simpl in ×.
apply sqrt_lt_1.
apply Cnorm_sqr_pos. apply Cnorm_sqr_pos.
unfold Cnorm_sqr. simpl. ring_simplify. do 2 rewrite Rplus_assoc. apply (Rplus_lt_compat_l (r^2)).
rewrite <- H1. ring_simplify. apply Rplus_le_lt_0_compat.
replace R0 with (2×0)%R by ring.
apply Rmult_le_compat_l. fourier. assumption. fourier.
rewrite S_INC.
apply Rlt_trans with (Cnorm (INC m)). exact IHle.
generalize (Cre_INC_pos m). generalize (Cim_INC_0 m).
intros H1 H2.
destruct (INC m). simpl in ×.
apply sqrt_lt_1.
apply Cnorm_sqr_pos. apply Cnorm_sqr_pos.
unfold Cnorm_sqr. simpl. ring_simplify. do 2 rewrite Rplus_assoc. apply (Rplus_lt_compat_l (r^2)).
rewrite <- H1. ring_simplify. apply Rplus_le_lt_0_compat.
replace R0 with (2×0)%R by ring.
apply Rmult_le_compat_l. fourier. assumption. fourier.
Qed.
Hint Resolve Cnorm_lt_INC: complex.

Lemma Cnorm_lt_1_INC : n:nat, (1 < n)%nat → 1 < Cnorm (INC n).
Proof.
intros n H.
induction n.
inversion H.
rewrite S_INC.
destruct n. inversion H. inversion H1.
rewrite S_INC in IHn.
rewrite S_INC.
generalize (Cre_INC_pos n). generalize (Cim_INC_0 n).
intros H2 H3.
destruct (INC n); simpl in ×.
rewrite <- sqrt_1. apply sqrt_lt_1. fourier. apply Cnorm_sqr_pos.
unfold Cnorm_sqr ; simpl.
rewrite <- H2.
apply Rminus_gt. unfold Cnorm_sqr. ring_simplify.
unfold Rminus ; rewrite Rplus_assoc ; apply Rplus_le_lt_0_compat.
apply Rmult_le_pos ; [| rewrite Rmult_1_r] ; assumption.
replace R0 with (4×0)%R by ring. fourier.
Qed.
Hint Resolve Cnorm_lt_1_INC : complex.

Lemma Cnorm_INC_lt : n m:nat, Cnorm (INC n) < Cnorm (INC m) → (n < m)%nat.
Proof.
double induction n m.
simpl. intro Habs. fourier.
intros n1 H1 H2. destruct n1. intuition. constructor. assert (Hind : (0<S n1 → 1 S n1)%nat). intuition.
apply Hind. apply H1. rewrite S_INC.
generalize (Cre_INC_pos n1). generalize (Cim_INC_0 n1). intros Hu Hs.
destruct (INC n1). simpl in ×. apply sqrt_lt_1. unfold Cnorm_sqr. simpl. apply Cnorm_sqr_pos.
unfold Cnorm_sqr. apply Cnorm_sqr_pos.
unfold Cnorm_sqr. simpl. rewrite <- Hu. ring_simplify. apply Rplus_le_lt_0_compat. apply Rplus_le_le_0_compat.
replace (r^2)%R with (Rsqr r) by (compute; ring). apply Rle_0_sqr.
replace R0 with (2×0)%R by ring.
apply Rmult_le_compat_l. fourier. assumption. fourier.
intros n0 H1 H2. rewrite S_INC in H2.
generalize (Cre_INC_pos n0). generalize (Cim_INC_0 n0). intros Hu Hs.
destruct (INC n0). simpl in ×. apply sqrt_lt_0 in H2. unfold Cnorm_sqr in ×. simpl in ×. rewrite <- Hu in H2.
ring_simplify in H2. assert (H : 0 (Rsqr (r+1))%R). apply Rle_0_sqr. destruct H. compute in H. ring_simplify in H.
assert (H0 : ( x: R, x > 0 → x < 0 → False)). intros. fourier. assert (Habs : ((0 < r ^ 2 + 2 × r + 1) → (r ^ 2 + 2 × r + 1 < 0)->False)%R).
apply H0. destruct Habs ; assumption.
rewrite H in H2. compute in H2. ring_simplify in H2. fourier.
apply Cnorm_sqr_pos. unfold Cnorm_sqr. simpl. apply Cnorm_sqr_pos.
intros n0 H1 n1 H3 H4.
assert (H : (n1<n0S n1 < S n0)%nat). intuition.
apply H.
apply H3.
do 2 rewrite S_INC in H4.
generalize (Cre_INC_pos n0). generalize (Cim_INC_0 n0). intros Hu Hs.
generalize (Cre_INC_pos n1). generalize (Cim_INC_0 n1). intros Hu1 Hs1.
destruct (INC n0) ; destruct (INC n1). simpl in ×. apply sqrt_lt_1. apply sqrt_lt_0 in H4.
apply Cnorm_sqr_pos.
apply Cnorm_sqr_pos.
apply Cnorm_sqr_pos.
apply Cnorm_sqr_pos.
rewrite <- Hu in ×. rewrite <- Hu1 in ×. apply sqrt_lt_0 in H4. ring_simplify in H4.
unfold Cnorm_sqr in ×. simpl in ×. ring_simplify in H4. ring_simplify.
generalize H4.
replace (r1 ^ 2 + 2 × r1 + 1)%R with (Rsqr (r1 + 1))%R by (compute; ring).
replace (r ^ 2 + 2 × r + 1)%R with (Rsqr (r + 1))%R by (compute; ring).
replace ( r1 ^ 2)%R with (Rsqr r1) by (compute ; ring).
replace ( r ^ 2)%R with (Rsqr r) by (compute ; ring).
intro H5. apply Rsqr_incrst_0 in H5. apply Rsqr_incrst_1. fourier.
exact Hs1. exact Hs. fourier. fourier. apply Cnorm_sqr_pos. apply Cnorm_sqr_pos.
Qed.
Hint Resolve Cnorm_INC_lt: complex.

Lemma Cnorm_le_INC : n m:nat, (n m)%nat
Cnorm (INC n) Cnorm (INC m).
Proof.
intros n m H.
induction H. right. reflexivity.
apply Rle_trans with (Cnorm (INC m)). exact IHle.
left. apply Cnorm_lt_INC. intuition.
Qed.
Hint Resolve Cnorm_le_INC : complex.

# INC/Cre/Cim

Lemma INC_not_0 : n:nat, INC n 0 → n 0%nat.
Proof.
induction n ; intuition.
Qed.
Hint Immediate INC_not_0 : complex.

Lemma not_0_INC : n:nat, n 0%natINC n 0.
Proof.
induction n. intuition.
intro H.
rewrite S_INC.
generalize (Cre_INC_pos n).
intro H1.
destruct (INC n). simpl in ×. rewrite <- Ceq.
simpl. intuition. fourier.
Qed.
Hint Resolve not_0_INC : complex.

Lemma not_INC : n m:nat, n mINC n INC m.
Proof.
double induction n m. intuition.
intros n1 H1 H2. intro H. apply H2. rewrite S_INC in H.
generalize (Cre_INC_pos n1). intro H3. destruct (INC n1). simpl in ×.
apply Ceq in H. elim H. intros H5 H6. simpl in ×. fourier.
intros n1 H1 H2. intro H. apply H2. rewrite S_INC in H.
generalize (Cre_INC_pos n1). intro H3. destruct (INC n1). simpl in ×.
apply Ceq in H. elim H. intros H5 H6. simpl in ×. fourier.
intros n0 H1 n1 H3 H4.
do 2 rewrite S_INC. assert ( H : (INC n1 INC n0INC n1 + 1 INC n0 + 1)).
intros temp1 temp2.
apply temp1.
exact temp2.
apply H.
apply H3.
intuition.
Qed.
Hint Resolve not_INC: complex.

Lemma Cre_let_1 : (f g : RR) (c : R × R),
Cre (let (a, b) := c in (f a +i g b)) = f (Cre c).
Proof.
intros.
destruct c. simpl. reflexivity.
Qed.

Lemma Cim_let_1 : (f g : RR) (c : R × R),
Cim (let (a, b) := c in (f a +i g b)) = g (Cim c).
Proof.
intros.
destruct c. simpl. reflexivity.
Qed.

Lemma Cre_let_2 : (f g : RRR) (c : R × R),
Cre (let (a, b) := c in (f a b +i g a b)) = f (Cre c) (Cim c).
Proof.
intros.
destruct c. simpl. reflexivity.
Qed.

Lemma Cim_let_2 : (f g : RRR) (c : R × R),
Cim (let (a, b) := c in (f a b +i g a b)) = g (Cre c) (Cim c).
Proof.
intros.
destruct c. simpl. reflexivity.
Qed.

Lemma Cim_mul : z1 z2, Cim (z1 × z2) = ((Cre z1) × (Cim z2) + (Cre z2) × (Cim z1))%R.
Proof.
intros z z' ; destruct z ; destruct z'.
compute ; field.
Qed.

Lemma Cre_mul : z1 z2, Cre (z1 × z2) = (Cre z1 × Cre z2 - Cim z1 × Cim z2)%R.
Proof.
intros z z' ; destruct z ; destruct z'.
compute ; field.
Qed.

Lemma Cim_inv_compat_0 : z, Cim z = 0%RCim (/z) = 0%R.
Proof.
intuition.
destruct z.
unfold Cinv.
simpl in ×.
rewrite H. replace (- 0 / (r × r + 0 × 0))%R with (0%R).
intuition. rewrite Ropp_0. unfold Rdiv. rewrite Rmult_0_l.
reflexivity.
Qed.

Lemma Cre_inv_compat_0 : z, Cre z = 0%RCre (/z) = 0%R.
Proof.
intuition.
destruct z.
unfold Cinv.
simpl in H.
rewrite H. unfold Rdiv. rewrite Rmult_0_l.
reflexivity.
Qed.

Lemma Cim_INC : n, Cim (INC n) = 0%R.
Proof.
intros n.
induction n.
intuition.
rewrite S_INC.
rewrite IHn. simpl. intuition.
Qed.

Lemma Cre_INC_INR : n, Cre (INC n) = INR n.
Proof.
induction n.
reflexivity.
rewrite IHn. rewrite S_INR. reflexivity.
Qed.

Lemma Cim_inv_INC : n, Cim (/ INC n) = 0%R.
Proof.
intros.
apply Cim_inv_compat_0.
apply Cim_INC.
Qed.

Lemma INC_inv_Cre_INR : n : nat, n 0%natCre (/INC n) = (/(INR n))%R.
Proof.
intros n Hn.
unfold Cinv.
simpl. repeat rewrite <- Cim_INC_0.
repeat rewrite Cre_INC_INR.
field. apply not_0_INR. exact Hn.
Qed.

Lemma INC_inv_Cim_INR : n : nat, n 0%natCim (/INC n) = 0%R.
Proof.
intros n Hn.
unfold Cinv.
simpl. repeat rewrite <- Cim_INC_0.
repeat rewrite Cre_INC_INR.
field. apply not_0_INR. exact Hn.
Qed.

# Cneq results

Lemma Cadd_neq_compat_l : z z', z' 0 → z + z' z.
Proof.
intros z z' z'_neq Hf ; apply z'_neq.
assert (H := Cadd_eq_compat_l (- z) _ _ Hf).
assumption.
Qed.

Lemma Cadd_neq_compat_r : z z', z' 0 → z' + z z.
Proof.
intros z z' z'_neq ; rewrite Cadd_comm ;
Qed.

# Compatibility of IRC and real/complex lemma

Lemma Cadd_IRC_compat_l : (r a b : R), r + (a +i b) = ((r + a)%R +i b).
Proof.
CusingR.
Qed.

Lemma Cadd_IRC_compat_r : (r a b : R), (a +i b) + r = ((a + r)%R +i b).
Proof.
CusingR.
Qed.

Lemma Cminus_IRC_compat_l : (r a b : R), r - (a +i b) = ((r - a)%R +i -b).
Proof.
CusingR.
Qed.
Hint Resolve Cminus_IRC_compat_l : complex.

Lemma Cminus_IRC_compat_r : (r a b : R), (a +i b) - r = ((a - r)%R +i b).
Proof.
CusingR_f.
Qed.
Hint Resolve Cminus_IRC_compat_r : complex.

Lemma Cmult_IRC_compat_l : r a b, (r × a +i r × b) = r × (a +i b).
Proof.
intros.
CusingR_f.
Qed.
Hint Resolve Cmult_IRC_compat_l : complex.

Lemma Cmult_IRC_compat_r : r a b, ( a × r +i b × r) = (a +i b) × r.
Proof.
intros.
CusingR_f.
Qed.
Hint Resolve Cmult_IRC_compat_r : complex.

Lemma Cadd_IRC_Rplus : (a b : R), IRC (Rplus a b) = Cadd a b.
Proof.
CusingR.
Qed.

Lemma Cminus_IRC_Rminus : (a b : R), IRC (a - b) = a - b.
Proof.
CusingR.
Qed.
Hint Resolve Cminus_IRC_Rminus : complex.

Lemma Cmult_IRC_Rmult : (a b : R), IRC (a × b) = a × b.
Proof.
intros.
CusingR_f ; assumption.
Qed.
Hint Resolve Cmult_IRC_Rmult : complex.

Lemma Cdiv_IRC_Rdiv : (a b : R), b 0%RIRC (a / b) = a / b.
Proof.
intros.
CusingR_f ; assumption.
Qed.
Hint Resolve Cdiv_IRC_Rdiv : complex.

Lemma Cinv_IRC_Rinv : (b : R), b 0%RIRC (/ b) = / b.
Proof.
intros.
CusingR_f ; assumption.
Qed.
Hint Resolve Cinv_IRC_Rinv : complex.

Lemma Cre_div_compat : (z : C) (r : R), r R0Cre (z / r) = (Cre z / r)%R.
Proof.
intros z r r_neq ; unfold Rdiv, Cdiv ; rewrite <- Cinv_IRC_Rinv ;
[apply Cre_mult_compat_r | assumption].
Qed.

Lemma Cim_div_compat : (z : C) (r : R), r R0Cim (z / r) = (Cim z / r)%R.
Proof.
intros z r r_neq ; unfold Rdiv, Cdiv ; rewrite <- Cinv_IRC_Rinv ;
[apply Cim_mult_compat_r | assumption].
Qed.

# Compatibility of Cconj with Cnorm_sqr

Lemma Cmod_conj_compat : z, Cre (z × Cconj z) = ((Cnorm z) ^ 2)%R
Cim ( z × Cconj z) = 0%R.
Proof.
intros z.
split ; CusingR1.
unfold Cnorm. rewrite Rmult_1_r. rewrite <- sqrt_mult.
rewrite sqrt_square.
unfold Cnorm_sqr. simpl. ring.
apply Cnorm_sqr_pos.
apply Cnorm_sqr_pos.
apply Cnorm_sqr_pos.
Qed.

# Compatibility of pow and Cpow

Lemma Cpow_Cre_Cim_0 : r n, Cre ((r +i 0%R) ^ n) = (r ^ n)%R Cim ((r +i 0%R) ^ n) = 0%R.
Proof.
induction n.
compute ; split ; reflexivity.
replace ((r +i 0%R) ^ S n) with ((r +i 0%R) ^ n × (r +i 0%R)) by (rewrite Cpow_S ; intuition).
simpl. destruct IHn as (IHn1, IHn2).
split ; simpl ; rewrite IHn1 ; rewrite IHn2 ; field.
Qed.

Lemma Cpow_Cre_0 : r n, Cre ((r +i 0%R) ^ n) = (r ^ n)%R.
Proof.
intros.
destruct (Cpow_Cre_Cim_0 r n).
assumption.
Qed.

Lemma Cpow_Cim_0 : r n, Cim ((r +i 0%R) ^ n) = 0%R.
Proof.
intros.
destruct (Cpow_Cre_Cim_0 r n).
assumption.
Qed.

Lemma nat_4_dec : n, k, (4 × k = n 4 × k + 1= n 4 × k + 2 = n 4 × k + 3 = n )%nat.
Proof.
induction n.
0%nat. left. intuition.
destruct IHn as [k [H | [H| [H|H]]]].
k. right. left. intuition.
k. right. right. left. intuition.
k. right. right. right. intuition.
(S k). left. intuition.
Qed.

Lemma Cpow_Cre_4_0 : n r, Cre ((0%R +i r) ^ (4 × n)) = (r ^ (4 × n))%R.
Proof.
intros.
induction n.
intuition. replace (4 × S n)%nat with (4 + 4 × n)%nat by ring.
rewrite Cpow_mul in ×. replace ((0%R +i r) ^ 4) with (r ^ 4 +i 0)%R in ×.
rewrite Cre_mul in ×. simpl (Cim (r ^ 4 +i 0))%R. ring_simplify.
rewrite IHn. simpl. field. CusingR_f.
Qed.

Lemma Cpow_Cim_4_0 : n r, Cim ((0%R +i r) ^ (4 × n)) = 0%R.
Proof.
intros ; induction n.
intuition. replace (4 × S n)%nat with (4 + 4 × n)%nat by ring.
rewrite Cpow_mul in ×. replace ((0%R +i r) ^ 4) with (r ^ 4 +i 0)%R in ×.
rewrite Cim_mul in ×. simpl (Cim (r ^ 4 +i 0))%R. ring_simplify.
rewrite IHn. simpl. ring. CusingR_f.
Qed.

Lemma Cpow_Cre_4_1 : n r, Cre ((0%R +i r) ^ (4 × n + 1)) = 0%R.
Proof.
intros.
rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0.
simpl ; field.
Qed.

Lemma Cpow_Cim_4_1 : n r, Cim ((0%R +i r) ^ (4 × n + 1)) = (r ^ (4 × n + 1))%R.
Proof.
rewrite Cim_mul. rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0.
Qed.

Lemma Cpow_Cre_4_2 : n r, Cre ((0%R +i r) ^ (4 × n + 2)) = (- r ^ (4 × n + 2))%R.
Proof.
intros.
rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0. ring_simplify.
simpl ( Cre ((0%R +i r) ^ 2)). ring_simplify. rewrite Rdef_pow_add.
ring.
Qed.

Lemma Cpow_Cim_4_2 : n r, Cim ((0%R +i r) ^ (4 × n + 2)) = 0%R.
Proof.
rewrite Cim_mul. rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0.
simpl. ring.
Qed.

Lemma Cpow_Cre_4_3 : n r, Cre ((0%R +i r) ^ (4 × n + 3)) = 0%R.
Proof.
intros.
rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0. ring_simplify.
simpl. ring.
Qed.

Lemma Cpow_Cim_4_3 : n r, Cim ((0%R +i r) ^ (4 × n + 3)) = (- r ^ (4 × n + 3))%R.
Proof.
intros.
rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0. ring_simplify.