Require Export Prelim.
Require Export RealAux.
Require Export Summation.

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

Declare Scope C_scope.
Delimit Scope C_scope with C.

Open Scope nat_scope.
Open Scope R_scope.
Open Scope C_scope.
Bind Scope nat_scope with nat.
Bind Scope R_scope with R.
Bind Scope C_scope with C.

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

Lemma RtoC_inj : ∀ (x y : R),
  RtoC x = RtoC y → x = y.

Lemma Ceq_dec (z1 z2 : C) : { z1 = z2 } + { z1 ≠ z2 }.

Lemma c_proj_eq : ∀ (c1 c2 : C), fst c1 = fst c2 → snd c1 = snd c2 → c1 = c2.

Ltac lca := eapply c_proj_eq; simpl; lra.

Definition Ci : C := (0,1).
Notation C0 := (RtoC 0).
Notation C1 := (RtoC 1).
Notation C2 := (RtoC 2).

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).

Fixpoint Cpow (c : C) (n : nat) : C :=
  match n with
  | 0%nat ⇒ 1
  | S n' ⇒ Cmult c (Cpow c n')
  end.

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.
Infix "^" := Cpow : C_scope.

Program Instance C_is_monoid : Monoid C :=
  { Gzero := C0
  ; Gplus := Cplus
  }.
Solve All Obligations with program_simpl; try lca.

Program Instance C_is_group : Group C :=
  { Gopp := Copp }.
Solve All Obligations with program_simpl; try lca.

Program Instance C_is_comm_group : Comm_Group C.
Solve All Obligations with program_simpl; lca.

Program Instance C_is_ring : Ring C :=
  { Gone := C1
  ; Gmult := Cmult
  }.
Solve All Obligations with program_simpl; lca.

Program Instance C_is_comm_ring : Comm_Ring C.
Solve All Obligations with program_simpl; lca.

Program Instance C_is_field : Field C :=
  { Ginv := Cinv }.

Program Instance C_is_vector_space : Vector_Space C C :=
  { Vscale := Cmult }.
Solve All Obligations with program_simpl; lca.

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).

Notation "a ^*" := (Cconj a) (at level 10) : C_scope.

Lemma Cmod_0 : Cmod 0 = R0.

Lemma Cmod_1 : Cmod 1 = R1.

Lemma Cmod_opp : ∀ x, Cmod (-x) = Cmod x.

Lemma Cmod_triangle : ∀ x y, Cmod (x + y) ≤ Cmod x + Cmod y.

Lemma Cmod_mult : ∀ x y, Cmod (x × y) = (Cmod x × Cmod y)%R.

Lemma Rmax_Cmod : ∀ x,
  Rmax (Rabs (fst x)) (Rabs (snd x)) ≤ Cmod x.

Lemma Cmod_2Rmax : ∀ x,
  Cmod x ≤ sqrt 2 × Rmax (Rabs (fst x)) (Rabs (snd x)).

Lemma C_neq_0 : ∀ c : C, c ≠ 0 → (fst c) ≠ 0 ∨ (snd c) ≠ 0.

Lemma Cplus_simplify : ∀ (a b c d : C),
    a = b → c = d → (a + c = b + d)%C.

Lemma Cmult_simplify : ∀ (a b c d : C),
    a = b → c = d → (a × c = b × d)%C.

Lemma RtoC_plus (x y : R) : RtoC (x + y) = RtoC x + RtoC y.

Lemma RtoC_opp (x : R) : RtoC (- x) = - RtoC x.

Lemma RtoC_minus (x y : R) : RtoC (x - y) = RtoC x - RtoC y.

Lemma RtoC_mult (x y : R) : RtoC (x × y) = RtoC x × RtoC y.

Lemma RtoC_inv (x : R) : (x ≠ 0)%R → RtoC (/ x) = / RtoC x.

Lemma RtoC_div (x y : R) : (y ≠ 0)%R → RtoC (x / y) = RtoC x / RtoC y.

Lemma Cplus_comm (x y : C) : x + y = y + x.

Lemma Cplus_assoc (x y z : C) : x + (y + z) = (x + y) + z.

Lemma Cplus_0_r (x : C) : x + 0 = x.

Lemma Cplus_0_l (x : C) : 0 + x = x.

Lemma Cplus_opp_r (x : C) : x + -x = 0.

Lemma Copp_plus_distr (z1 z2 : C) : - (z1 + z2) = (- z1 + - z2).

Lemma Copp_minus_distr (z1 z2 : C) : - (z1 - z2) = z2 - z1.

Lemma Cmult_comm (x y : C) : x × y = y × x.

Lemma Cmult_assoc (x y z : C) : x × (y × z) = (x × y) × z.

Lemma Cmult_0_r (x : C) : x × 0 = 0.

Lemma Cmult_0_l (x : C) : 0 × x = 0.

Lemma Cmult_1_r (x : C) : x × 1 = x.

Lemma Cmult_1_l (x : C) : 1 × x = x.

Lemma Cinv_r (r : C) : r ≠ 0 → r × /r = 1.

Lemma Cinv_l (r : C) : r ≠ 0 → /r × r = 1.

Lemma Cmult_plus_distr_l (x y z : C) : x × (y + z) = x × y + x × z.

Lemma Cmult_plus_distr_r (x y z : C) : (x + y) × z = x × z + y × z.

Lemma Copp_0 : Copp 0 = 0.

Lemma Cmod_m1 : Cmod (Copp 1) = 1.

Lemma Cmod_eq_0 : ∀ x, Cmod x = 0 → x = 0.

Lemma Cmod_ge_0 : ∀ x, 0 ≤ Cmod x.

Lemma Cmod_gt_0 :
  ∀ (x : C), x ≠ 0 ↔ 0 < Cmod x.

Lemma Cmod_R : ∀ x : R, Cmod x = Rabs x.

Lemma Cmod_inv : ∀ x : C, x ≠ 0 → Cmod (/ x) = Rinv (Cmod x).

Lemma Cmod_div (x y : C) : y ≠ 0 → Cmod (x / y) = Rdiv (Cmod x) (Cmod y).

Lemma Cmod_real : ∀ (c : C),
  fst c ≥ 0 → snd c = 0 → Cmod c = fst c.

Lemma Cmult_neq_0 (z1 z2 : C) : z1 ≠ 0 → z2 ≠ 0 → z1 × z2 ≠ 0.

Lemma Cminus_eq_contra : ∀ r1 r2 : C, r1 ≠ r2 → r1 - r2 ≠ 0.

Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.

Add Field C_field_field : C_field_theory.

Lemma Ci2 : Ci × Ci = -C1.
Lemma Copp_mult_distr_r : ∀ c1 c2 : C, - (c1 × c2) = c1 × - c2.
Lemma Copp_mult_distr_l : ∀ c1 c2 : C, - (c1 × c2) = - c1 × c2.
Lemma Cplus_opp_l : ∀ c : C, - c + c = 0.
Lemma Cdouble : ∀ c : C, 2 × c = c + c.
Lemma Copp_involutive: ∀ c : C, - - c = c.

Lemma C0_imp : ∀ c : C, c ≠ 0 → (fst c ≠ 0 ∨ snd c ≠ 0)%R.
Lemma C0_fst_neq : ∀ (c : C), fst c ≠ 0 → c ≠ 0.
Lemma C0_snd_neq : ∀ (c : C), snd c ≠ 0 → c ≠ 0.
Lemma RtoC_neq : ∀ (r : R), r ≠ 0 → RtoC r ≠ 0.

Lemma Copp_neq_0_compat: ∀ c : C, c ≠ 0 → (- c)%C ≠ 0.

Lemma C1_neq_C0 : C1 ≠ C0.

Lemma Cconj_neq_0 : ∀ c : C, c ≠ 0 → c^* ≠ 0.

Lemma nonzero_div_nonzero : ∀ c : C, c ≠ C0 → / c ≠ C0.

Lemma div_real : ∀ (c : C),
  snd c = 0 → snd (/ c) = 0.

Lemma eq_neg_implies_0 : ∀ (c : C),
  (-C1 × c)%C = c → c = C0.

Lemma Cinv_mult_distr : ∀ c1 c2 : C, c1 ≠ 0 → c2 ≠ 0 → / (c1 × c2) = / c1 × / c2.

Local Open Scope nat_scope.

Lemma big_sum_rearrange : ∀ (n : nat) (f g : nat → nat → C),
  (∀ x y, x ≤ y → f x y = (-C1) × (g (S y) x))%G →
  (∀ x y, y ≤ x → f (S x) y = (-C1) × (g y x))%G →
  big_sum (fun i ⇒ big_sum (fun j ⇒ f i j) n) (S n) =
  (-C1 × (big_sum (fun i ⇒ big_sum (fun j ⇒ g i j) n) (S n)))%G.

Local Close Scope nat_scope.

Lemma big_sum_ge_0 : ∀ f n, (∀ x, 0 ≤ fst (f x)) → (0 ≤ fst (big_sum f n))%R.

Lemma big_sum_gt_0 : ∀ f n, (∀ x, 0 ≤ fst (f x)) →
                              (∃ y : nat, (y < n)%nat ∧ 0 < fst (f y)) →
                              0 < fst (big_sum f n).

Lemma big_sum_member_le : ∀ (f : nat → C) (n : nat), (∀ x, 0 ≤ fst (f x)) →
                      (∀ x, (x < n)%nat → fst (f x) ≤ fst (big_sum f n)).

Lemma big_sum_squeeze : ∀ (f : nat → C) (n : nat),
  (∀ x, (0 ≤ fst (f x)))%R → big_sum f n = C0 →
  (∀ x, (x < n)%nat → fst (f x) = fst C0).

Lemma big_sum_snd_0 : ∀ n f, (∀ x, snd (f x) = 0) → snd (big_sum f n) = 0.

Lemma Rsum_big_sum : ∀ n (f : nat → R),
  fst (big_sum (fun i ⇒ RtoC (f i)) n) = big_sum f n.

Lemma big_sum_Cmod_0_all_0 : ∀ (f : nat → C) (n : nat),
  big_sum (fun i ⇒ Cmod (f i)) n = 0 →
  ∀ i, (i < n)%nat → f i = C0.

Lemma big_sum_triangle : ∀ f n,
  Cmod (big_sum f n) ≤ big_sum (fun i ⇒ Cmod (f i)) n.

Lemma RtoC_pow : ∀ r n, (RtoC r) ^ n = RtoC (r ^ n).

Lemma Cpow_nonzero : ∀ (r : R) (n : nat), (r ≠ 0 → r ^ n ≠ C0)%C.

Lemma Cpow_add : ∀ (c : C) (n m : nat), (c ^ (n + m) = c^n × c^m)%C.

Lemma Cpow_mult : ∀ (c : C) (n m : nat), (c ^ (n × m) = (c ^ n) ^ m)%C.

Lemma Cpow_inv : ∀ (c : C) (n : nat), (∀ n', (n' ≤ n)%nat → c ^ n' ≠ 0) → (/ c) ^ n = / (c ^ n).

Lemma Cpow_add_r : ∀ (c : C) (a b : nat), c ^ (a + b) = c ^ a × c ^ b.

Lemma Cpow_mul_l : ∀ (c1 c2 : C) (n : nat), (c1 × c2) ^ n = c1 ^ n × c2 ^ n.

Lemma Cmod_pow : ∀ x n, Cmod (x ^ n) = ((Cmod x) ^ n)%R.

Lemma Cmod_Cconj : ∀ c : C, Cmod (c^*) = Cmod c.

Lemma Cmod_real_pos :
  ∀ x : C,
    snd x = 0 →
    fst x ≥ 0 →
    x = Cmod x.

Lemma Cmod_sqr : ∀ c : C, (Cmod c ^2 = c^* × c)%C.

Lemma Cmod_switch : ∀ (a b : C),
  Cmod (a - b) = Cmod (b - a).

Lemma Cmod_triangle_le : ∀ (a b : C) (ϵ : R),
  Cmod a + Cmod b < ϵ → Cmod (a + b) < ϵ.

Lemma Cmod_triangle_diff : ∀ (a b c : C) (ϵ : R),
  Cmod (c - b) + Cmod (b - a) < ϵ → Cmod (c - a) < ϵ.

Lemma Cconj_R : ∀ r : R, r^* = r.
Lemma Cconj_0 : 0^* = 0.
Lemma Cconj_opp : ∀ C, (- C)^* = - (C^*).
Lemma Cconj_rad2 : (/ √2)^* = / √2.
Lemma Cplus_div2 : /2 + /2 = 1.
Lemma Cconj_involutive : ∀ c, (c^*)^* = c.
Lemma Cconj_plus_distr : ∀ (x y : C), (x + y)^* = x^* + y^*.
Lemma Cconj_mult_distr : ∀ (x y : C), (x × y)^* = x^* × y^*.
Lemma Cconj_minus_distr : ∀ (x y : C), (x - y)^* = x^* - y^*.

Lemma Cmult_conj_real : ∀ (c : C), snd (c × c^*) = 0.

Lemma Cconj_simplify : ∀ (c1 c2 : C), c1^* = c2^* → c1 = c2.

Lemma Csqrt_sqrt : ∀ x : R, 0 ≤ x → √ x × √ x = x.

Lemma Csqrt2_sqrt : √ 2 × √ 2 = 2.

Lemma Cinv_sqrt2_sqrt : /√2 × /√2 = /2.

Lemma Csqrt_inv : ∀ (r : R), 0 < r → RtoC (√ (/ r)) = (/ √ r).

Lemma Csqrt2_inv : RtoC (√ (/ 2)) = (/ √ 2).

Lemma Csqrt_sqrt_inv : ∀ (r : R), 0 < r → (√ r × √ / r) = 1.

Lemma Csqrt2_sqrt2_inv : (√ 2 × √ / 2) = 1.

Lemma Csqrt2_inv_sqrt2 : ((√ / 2) × √ 2) = 1.

Lemma Csqrt2_inv_sqrt2_inv : ((√ / 2) × (√ / 2)) = /2.

Lemma Csqrt2_neq_0 : (RtoC (√ 2) ≠ 0)%C.

Definition Cexp (θ : R) : C := (cos θ, sin θ).

Lemma Cexp_0 : Cexp 0 = 1.

Lemma Cexp_add: ∀ (x y : R), Cexp (x + y) = Cexp x × Cexp y.

Lemma Cexp_neg : ∀ θ, Cexp (- θ) = / Cexp θ.

Lemma Cexp_plus_PI : ∀ x,
  Cexp (x + PI) = (- (Cexp x))%C.

Lemma Cexp_minus_PI: ∀ x : R, Cexp (x - PI) = (- Cexp x)%C.

Lemma Cexp_nonzero : ∀ θ, Cexp θ ≠ 0.

Lemma Cexp_mul_neg_l : ∀ θ, Cexp (- θ) × Cexp θ = 1.

Lemma Cexp_mul_neg_r : ∀ θ, Cexp θ × Cexp (-θ) = 1.

Lemma Cexp_pow : ∀ θ k, Cexp θ ^ k = Cexp (θ × INR k).
  Local Opaque INR.
  Local Transparent INR.

Lemma Cexp_conj_neg : ∀ θ, (Cexp θ)^* = Cexp (-θ)%R.

Lemma Cmod_Cexp : ∀ θ, Cmod (Cexp θ) = 1.

Lemma Cmod_Cexp_alt : ∀ θ, Cmod (1 - Cexp (2 × θ)) = Cmod (2 × (sin θ)).

Lemma Cexp_PI : Cexp PI = -1.

Lemma Cexp_PI2 : Cexp (PI/2) = Ci.

Lemma Cexp_2PI : Cexp (2 × PI) = 1.

Lemma Cexp_3PI2: Cexp (3 × PI / 2) = - Ci.

Lemma Cexp_PI4 : Cexp (PI / 4) = /√2 + /√2 × Ci.

Lemma Cexp_PIm4 : Cexp (- PI / 4) = /√2 - /√2 × Ci.

Lemma Cexp_0PI4 : Cexp (0 × PI / 4) = 1.

Lemma Cexp_1PI4 : Cexp (1 × PI / 4) = /√2 + /√2 × Ci.

Lemma Cexp_2PI4 : Cexp (2 × PI / 4) = Ci.

Lemma Cexp_3PI4 : Cexp (3 × PI / 4) = -/√2 + /√2 × Ci.

Lemma Cexp_4PI4 : Cexp (4 × PI / 4) = -1.

Lemma Cexp_5PI4 : Cexp (5 × PI / 4) = -/√2 - /√2 × Ci.

Lemma Cexp_6PI4 : Cexp (6 × PI / 4) = -Ci.

Lemma Cexp_7PI4 : Cexp (7 × PI / 4) = /√2 - /√2 × Ci.

Lemma Cexp_8PI4 : Cexp (8 × PI / 4) = 1.

Lemma Cexp_PI4_m8 : ∀ (k : Z), Cexp (IZR (k - 8) × PI / 4) = Cexp (IZR k × PI / 4).

Lemma Cexp_2nPI : ∀ (k : Z), Cexp (IZR (2 × k) × PI) = 1.

Lemma Cexp_mod_2PI : ∀ (k : Z), Cexp (IZR k × PI) = Cexp (IZR (k mod 2) × PI).

Lemma Cexp_mod_2PI_scaled : ∀ (k sc : Z),
  (sc ≠ 0)%Z →
  Cexp (IZR k × PI / IZR sc) = Cexp (IZR (k mod (2 × sc)) × PI / IZR sc).

Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4
  Cexp_1PI4 Cexp_2PI4 Cexp_3PI4 Cexp_4PI4 Cexp_5PI4 Cexp_6PI4 Cexp_7PI4 Cexp_8PI4
  Cexp_add Cexp_neg Cexp_plus_PI Cexp_minus_PI : Cexp_db.

Opaque C.

Lemma Cminus_unfold : ∀ c1 c2, (c1 - c2 = c1 + -c2)%C.
Lemma Cdiv_unfold : ∀ c1 c2, (c1 / c2 = c1 ×/ c2)%C.

Ltac nonzero :=
  repeat split;
  repeat
    match goal with
    | |- not (@eq _ (Copp _) (RtoC (IZR Z0))) ⇒ apply Copp_neq_0_compat
    | |- not (@eq _ (Cpow _ _) (RtoC (IZR Z0))) ⇒ apply Cpow_nonzero
    | |- not (@eq _ Ci (RtoC (IZR Z0))) ⇒ apply C0_snd_neq; simpl
    | |- not (@eq _ (Cexp _) (RtoC (IZR Z0))) ⇒ apply Cexp_nonzero
    | |- not (@eq _ _ (RtoC (IZR Z0))) ⇒ apply RtoC_neq
    end;
  repeat
    match goal with
    | |- not (@eq _ (sqrt (pow _ _)) (IZR Z0)) ⇒ rewrite sqrt_pow
    | |- not (@eq _ (pow _ _) (IZR Z0)) ⇒ apply pow_nonzero; try apply RtoC_neq
    | |- not (@eq _ (sqrt _) (IZR Z0)) ⇒ apply sqrt_neq_0_compat
    | |- not (@eq _ (Rinv _) (IZR Z0)) ⇒ apply Rinv_neq_0_compat
    | |- not (@eq _ (Rmult _ _) (IZR Z0)) ⇒ apply Rmult_integral_contrapositive_currified
    end;
  repeat
    match goal with
    | |- Rlt (IZR Z0) (Rmult _ _) ⇒ apply Rmult_lt_0_compat
    | |- Rlt (IZR Z0) (Rinv _) ⇒ apply Rinv_0_lt_compat
    | |- Rlt (IZR Z0) (pow _ _) ⇒ apply pow_lt
    end;
  match goal with
  | |- not (@eq _ _ _) ⇒ lra
  | |- Rlt _ _ ⇒ lra
  | |- Rle _ _ ⇒ lra
  end.

Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2
     Cinv_sqrt2_sqrt Cplus_div2
     Cplus_0_l Cplus_0_r Cplus_opp_r Cplus_opp_l Copp_0 Copp_involutive
     Cmult_0_l Cmult_0_r Cmult_1_l Cmult_1_r : C_db.

Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db.
Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db.
Hint Rewrite Cinv_l Cinv_r using nonzero : C_db.
Hint Rewrite Cinv_mult_distr using nonzero : C_db.

Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0
             Cconj_R Cmult_1_l Cmult_1_r : C_db_light.

Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l
              Copp_involutive : Cdist_db.

Hint Rewrite <- RtoC_opp RtoC_mult RtoC_plus : RtoC_db.
Hint Rewrite <- RtoC_inv using nonzero : RtoC_db.
Hint Rewrite RtoC_pow : RtoC_db.

Ltac Csimpl :=
  repeat match goal with
  | _ ⇒ rewrite Cmult_0_l
  | _ ⇒ rewrite Cmult_0_r
  | _ ⇒ rewrite Cplus_0_l
  | _ ⇒ rewrite Cplus_0_r
  | _ ⇒ rewrite Cmult_1_l
  | _ ⇒ rewrite Cmult_1_r
  | _ ⇒ rewrite Cconj_R
  end.

Ltac C_field_simplify := repeat field_simplify_eq [ Csqrt2_sqrt Csqrt2_inv Ci2].
Ltac C_field := C_field_simplify; nonzero; trivial.

Ltac has_term t exp :=
  match exp with
    | context[t] ⇒ idtac
  end.

Ltac group_radicals :=
  repeat rewrite Cconj_opp;
  repeat rewrite Cconj_rad2;
  repeat rewrite <- Copp_mult_distr_l;
  repeat rewrite <- Copp_mult_distr_r;
  repeat match goal with
  | _ ⇒ rewrite Cinv_sqrt2_sqrt
  | |- context [ ?x × ?y ] ⇒ tryif has_term (√ 2) x then fail
                            else (has_term (√ 2) y; rewrite (Cmult_comm x y))
  | |- context [ ?x × ?y × ?z ] ⇒
    tryif has_term (√ 2) y then fail
    else (has_term (√ 2) x; has_term (√ 2) z; rewrite <- (Cmult_assoc x y z))
  | |- context [ ?x × (?y × ?z) ] ⇒
    has_term (√ 2) x; has_term (√ 2) y; rewrite (Cmult_assoc x y z)
  end.

Ltac cancel_terms t :=
  repeat rewrite Cmult_plus_distr_l;
  repeat rewrite Cmult_plus_distr_r;
  repeat match goal with
  | _ ⇒ rewrite Cmult_1_l
  | _ ⇒ rewrite Cmult_1_r
  | _ ⇒ rewrite Cinv_r; try nonzero
  | _ ⇒ rewrite Cinv_l; try nonzero
  | |- context[(?x × ?y)%C] ⇒ tryif has_term (/ t)%C y then fail else has_term (/ t)%C x; has_term t y;
                                    rewrite (Cmult_comm x y)
  | |- context[(?x × (?y × ?z))%C] ⇒ has_term t x; has_term (/ t)%C y;
                                    rewrite (Cmult_assoc x y z)
  | |- context[(?x × (?y × ?z))%C] ⇒ tryif has_term t y then fail else has_term t x; has_term (/ t)%C z;
                                    rewrite (Cmult_comm y z)
  | |- context[(?x × ?y × ?z)%C] ⇒ tryif has_term t x then fail else has_term t y; has_term (/ t)%C z;
                                    rewrite <- (Cmult_assoc x y z)
  end.

Ltac group_Cexp :=
  repeat rewrite <- Cexp_neg;
  repeat match goal with
  | _ ⇒ rewrite <- Cexp_add
  | _ ⇒ rewrite <- Copp_mult_distr_l
  | _ ⇒ rewrite <- Copp_mult_distr_r
  | |- context [ ?x × ?y ] ⇒ tryif has_term Cexp x then fail
                            else (has_term Cexp y; rewrite (Cmult_comm x y))
  | |- context [ ?x × ?y × ?z ] ⇒
    tryif has_term Cexp y then fail
    else (has_term Cexp x; has_term Cexp z; rewrite <- (Cmult_assoc x y z))
  | |- context [ ?x × (?y × ?z) ] ⇒
    has_term Cexp x; has_term Cexp y; rewrite (Cmult_assoc x y z)
  end.