Require Export NRootIR.

Section Complex_Numbers.
Record CC_set : Type :=
  {ℜ : IR;
   ℑ : IR}.

Definition cc_ap (x y : CC_set) : CProp := ℜ x [#] ℜ y or ℑ x [#] ℑ y.

Definition cc_eq (x y : CC_set) : Prop := ℜ x [=] ℜ y ∧ ℑ x [=] ℑ y.

Lemma cc_is_CSetoid : is_CSetoid _ cc_eq cc_ap.
Proof.
 apply Build_is_CSetoid.
    unfold irreflexive in |- ×.
    intros. elim x. intros x1 x2. unfold cc_ap in |- ×. simpl in |- ×.
    intro H. elim H; clear H; intros H.
    cut (Not (x1 [#] x1)). intros H0. elim (H0 H). apply ap_irreflexive_unfolded.
      cut (Not (x2 [#] x2)). intros H0. elim (H0 H). apply ap_irreflexive_unfolded.
     unfold Csymmetric in |- ×.
   intros x y. elim x. intros x1 x2. elim y. intros y1 y2. unfold cc_ap in |- ×.
   simpl in |- ×. intros H. elim H; clear H; intros H.
   left. apply ap_symmetric_unfolded. auto.
    right. apply ap_symmetric_unfolded. auto.
   unfold cotransitive in |- ×.
  intros x y. elim x. intros x1 x2. elim y. intros y1 y2. unfold cc_ap in |- ×.
  simpl in |- ×. intro H. intro. elim z. intros z1 z2. simpl in |- ×. intros.
  elim H; clear H; intros H.
   cut (x1 [#] z1 or z1 [#] y1). intro H0.
    elim H0; clear H0; intros H0. left. left. auto. right. left. auto.
     apply ap_cotransitive_unfolded. auto.
   cut (x2 [#] z2 or z2 [#] y2). intro H0.
   elim H0; clear H0; intros H0. left. right. auto. right. right. auto.
    apply ap_cotransitive_unfolded. auto.
  unfold tight_apart in |- ×.
 intros x y. elim x. intros x1 x2. elim y. intros y1 y2.
 unfold cc_ap in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split.
 intros. split.
  apply not_ap_imp_eq. intro. apply H. left. auto.
   apply not_ap_imp_eq. intro. apply H. right. auto.
  intros. elim H. clear H. intros H H0. intro H1. elim H1; clear H1; intros H1.
 cut (Not (x1 [#] y1)). intro. elim (H2 H1). apply eq_imp_not_ap. auto.
   cut (Not (x2 [#] y2)). intro. elim (H2 H1). apply eq_imp_not_ap. auto.
Qed.

Definition cc_csetoid := Build_CSetoid CC_set cc_eq cc_ap cc_is_CSetoid.

Definition cc_plus x y := Build_CC_set (ℜ x[+]ℜ y) (ℑ x[+]ℑ y).

Definition cc_mult x y := Build_CC_set (ℜ x[*]ℜ y[-]ℑ x[*]ℑ y) (ℜ x[*]ℑ y[+]ℑ x[*]ℜ y).

Definition cc_zero := Build_CC_set ZeroR ZeroR.

Definition cc_one := Build_CC_set OneR ZeroR.

Definition cc_i := Build_CC_set ZeroR OneR.

Definition cc_inv (x : CC_set) : CC_set := Build_CC_set [--] (ℜ x) [--] (ℑ x).


Lemma cc_inv_strext : un_op_strext cc_csetoid cc_inv.
Proof.
 unfold un_op_strext in |- ×. unfold fun_strext in |- ×.
 intros x y. elim x. elim y.
 simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×. do 4 intro. intro H.
 elim H; clear H; intros.
  left. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto.
  right. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto.
Qed.

Lemma cc_plus_strext : bin_op_strext cc_csetoid cc_plus.
Proof.
 unfold bin_op_strext in |- ×. unfold bin_fun_strext in |- ×.
 intros x1 x2 y1 y2. elim x1. elim x2. elim y1. elim y2.
 simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×. do 8 intro. intro H.
 elim H; clear H; intros H.
  elim (bin_op_strext_unfolded _ _ _ _ _ _ H); intros.
   left. left. auto. right. left. auto.
   elim (bin_op_strext_unfolded _ _ _ _ _ _ H); intros.
  left. right. auto. right. right. auto.
Qed.

Lemma cc_mult_strext : bin_op_strext cc_csetoid cc_mult.
Proof.
 unfold bin_op_strext in |- ×. unfold bin_fun_strext in |- ×.
 intros x1 x2 y1 y2. elim x1. elim x2. elim y1. elim y2.
 simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×. do 8 intro. intro H.
 elim H; clear H; intros H.
  elim (bin_op_strext_unfolded _ (cg_minus_is_csetoid_bin_op _) _ _ _ _ H); intros H0.
   elim (bin_op_strext_unfolded _ _ _ _ _ _ H0); intros H1.
    left. left. auto. right. left. auto.
    cut (Im3[*]Im1 [#] Im2[*]Im0). intro H1.
   elim (bin_op_strext_unfolded _ _ _ _ _ _ H1); intros H2.
    left. right. auto. right. right. auto.
    auto.
 elim (bin_op_strext_unfolded _ _ _ _ _ _ H); intros H0.
  elim (bin_op_strext_unfolded _ _ _ _ _ _ H0); intros H1.
   left. left. auto. right. right. auto.
   elim (bin_op_strext_unfolded _ _ _ _ _ _ H0); intros.
  left. right. auto. right. left. auto.
Qed.

Definition cc_inv_op := Build_CSetoid_un_op _ _ cc_inv_strext.

Definition cc_plus_op := Build_CSetoid_bin_op _ _ cc_plus_strext.

Definition cc_mult_op := Build_CSetoid_bin_op _ _ cc_mult_strext.

Lemma cc_csg_associative : associative cc_plus_op.
Proof.
 unfold associative in |- ×. intros. elim x. elim y. elim z. intros.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Lemma cc_cr_mult_associative : associative cc_mult_op.
Proof.
 unfold associative in |- ×. intros. elim x. elim y. elim z. intros.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Definition cc_csemi_grp := Build_CSemiGroup cc_csetoid _ cc_csg_associative.

Lemma cc_cm_proof : is_CMonoid cc_csemi_grp cc_zero.
Proof.
 apply Build_is_CMonoid.
  unfold is_rht_unit in |- ×. intros. elim x. intros.
  simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
  unfold is_lft_unit in |- ×. intros. elim x. intros.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Definition cc_cmonoid := Build_CMonoid _ _ cc_cm_proof.

Lemma cc_cg_proof : is_CGroup cc_cmonoid cc_inv_op.
Proof.
 unfold is_CGroup in |- ×. intros. elim x. intros.
 split.
  simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
  simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Lemma cc_cr_dist : distributive cc_mult_op cc_plus_op.
Proof.
 unfold distributive in |- ×. intros. elim x. elim y. elim z. intros.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Lemma cc_cr_non_triv : cc_ap cc_one cc_zero.
Proof.
 unfold cc_ap in |- ×. simpl in |- ×. left. apply Greater_imp_ap. apply pos_one.
Qed.

Definition cc_cgroup := Build_CGroup cc_cmonoid cc_inv_op cc_cg_proof.

Definition cc_cabgroup : CAbGroup.
Proof.
 apply Build_CAbGroup with cc_cgroup.
 red in |- *; unfold commutes in |- ×.
 intros.
 elim x; elim y; split; simpl in |- *; algebra.
Defined.

Lemma cc_cr_mult_mon : is_CMonoid
   (Build_CSemiGroup (csg_crr cc_cgroup) _ cc_cr_mult_associative) cc_one.
Proof.
 apply Build_is_CMonoid.
  unfold is_rht_unit in |- ×.
  intros. elim x. intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×.
  split; rational.
 unfold is_lft_unit in |- ×.
 intros. elim x. intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×.
 split; rational.
Qed.

Lemma cc_mult_commutes : commutes cc_mult_op.
Proof.
 unfold commutes in |- ×.
 intros. elim x. intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×.
 split; rational.
Qed.

Lemma cc_isCRing : is_CRing cc_cabgroup cc_one cc_mult_op.
Proof.
 apply Build_is_CRing with cc_cr_mult_associative.
    exact cc_cr_mult_mon.
   exact cc_mult_commutes.
  exact cc_cr_dist.
 exact cc_cr_non_triv.
Qed.

Definition cc_cring : CRing := Build_CRing _ _ _ cc_isCRing.

Lemma cc_ap_zero : ∀ z : cc_cring, z [#] [0] → ℜ z [#] [0] or ℑ z [#] [0].
Proof.
 intro z. unfold cc_ap in |- ×. intuition.
Qed.

Lemma cc_inv_aid : ∀ x y : IR, x [#] [0] or y [#] [0] → x[^]2[+]y[^]2 [#] [0].
Proof.
 intros x y H.
 apply Greater_imp_ap.
 elim H; clear H; intros.
  apply plus_resp_pos_nonneg. apply pos_square. auto. apply sqr_nonneg.
   apply plus_resp_nonneg_pos. apply sqr_nonneg. apply pos_square. auto.
Qed.

Lemma cc_inv_aid2 : ∀ (x y : IR) (H : x [#] [0] or y [#] [0]),
 (x[/] _[//]cc_inv_aid _ _ H) [#] [0] or ( [--]y[/] _[//]cc_inv_aid _ _ H) [#] [0].
Proof.
 intros x y H.
 elim H; intro H0.
  left.
  apply div_resp_ap_zero_rev. auto.
  right. apply div_resp_ap_zero_rev. apply inv_resp_ap_zero. auto.
Qed.


Definition cc_recip : ∀ z : cc_cring, z [#] [0] → cc_cring.
Proof.
 intros z z_.
 apply (Build_CC_set (ℜ z[/] _[//]cc_inv_aid _ _ z_) ( [--] (ℑ z) [/] _[//]cc_inv_aid _ _ z_)).
Defined.

Lemma cc_cfield_proof : is_CField cc_cring cc_recip.
Proof.
 unfold is_CField in |- ×. unfold is_inverse in |- ×.
 intro. elim x. intros x1 x2 Hx.
 split; simpl in |- *; unfold cc_eq in |- *; simpl in |- *; split; rational.
Qed.

Lemma cc_Recip_proof : ∀ x y x_ y_, cc_recip x x_ [#] cc_recip y y_ → x [#] y.
Proof.
 intro. elim x. intros x1 x2 y.
 intro Hx. elim y. intros y1 y2 Hy.
 simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×. intros H.
 elim H; clear H; intros H.
  cut (x1 [#] y1 or x1[^]2[+]x2[^]2 [#] y1[^]2[+]y2[^]2). intro H0.
   elim H0; clear H0; intros H0.
    left. auto.
    cut (x1[^]2 [#] y1[^]2 or x2[^]2 [#] y2[^]2). intro H1.
    elim H1; clear H1; intros.
     left. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto.
     right. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto.
    apply bin_op_strext_unfolded with (csg_op (c:=IR)). auto.
   apply div_strext with (cc_inv_aid x1 x2 Hx) (cc_inv_aid y1 y2 Hy). auto.
  cut ( [--]x2 [#] [--]y2 or x1[^]2[+]x2[^]2 [#] y1[^]2[+]y2[^]2). intro H0.
  elim H0; clear H0; intros H0.
   right. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto.
   cut (x1[^]2 [#] y1[^]2 or x2[^]2 [#] y2[^]2). intro H1.
   elim H1; clear H1; intros H1.
    left. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto.
    right. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto.
   apply bin_op_strext_unfolded with (csg_op (c:=IR)). auto.
  apply div_strext with (cc_inv_aid x1 x2 Hx) (cc_inv_aid y1 y2 Hy). auto.
Qed.

Opaque cc_recip.
Opaque cc_inv.

Definition cc_cfield := Build_CField _ _ cc_cfield_proof cc_Recip_proof.

Definition C := cc_cfield.

Definition cc_set_CC : IR → IR → C := Build_CC_set.

Definition cc_IR (x : IR) : C := cc_set_CC x [0].

Definition CC_conj : C → C := fun z : CC_set ⇒
  match z with
  | Build_CC_set Re0 Im0 ⇒ Build_CC_set Re0 [--]Im0
  end.


Definition AbsCC (z : C) : IR := sqrt (ℜ z[^]2[+]ℑ z[^]2) (cc_abs_aid _ (ℜ z) (ℑ z)).

Lemma TwoCC_ap_zero : (Two:C) [#] [0].
Proof.
 simpl in |- ×. unfold cc_ap in |- ×.
 simpl in |- ×. left.
 astepl (Two:IR).
 apply Greater_imp_ap. apply pos_two.
Qed.

End Complex_Numbers.


Definition i : C := cc_i.

Infix "[+I*]" := cc_set_CC (at level 48, no associativity).

Section I_properties.

Lemma I_square : i[*]i [=] [--][1].
Proof.
 simpl in |- ×. unfold cc_mult in |- ×. simpl in |- ×. unfold cc_inv in |- ×. simpl in |- ×.
 split. simpl in |- ×. rational. simpl in |- ×. rational.
Qed.

Hint Resolve I_square: algebra.

Lemma I_square' : i[^]2 [=] [--][1].
Proof.
 Step_final (i[*]i).
Qed.

Lemma I_recip_lft : [--]i[*]i [=] [1].
Proof.
 astepl ( [--] (i[*]i)).
 Step_final ( [--][--] ([1]:C)).
Qed.

Lemma I_recip_rht : i[*][--]i [=] [1].
Proof.
 astepl ( [--] (i[*]i)).
 Step_final ( [--][--] ([1]:C)).
Qed.

Lemma mult_I : ∀ x y : IR, (x[+I*]y) [*]i [=] [--]y[+I*]x.
Proof.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Lemma I_wd : ∀ x x' y y' : IR, x [=] x' → y [=] y' → x[+I*]y [=] x'[+I*]y'.
Proof.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. algebra.
Qed.

Lemma calculate_norm : ∀ x y : IR, (x[+I*]y) [*]CC_conj (x[+I*]y) [=] cc_IR (x[^]2[+]y[^]2).
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Lemma calculate_Re : ∀ c : C, cc_IR (ℜ c) [*]Two [=] c[+]CC_conj c.
Proof.
 intros. elim c. intros x y. intros.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Lemma calculate_Im : ∀ c : C, cc_IR (ℑ c) [*] (Two[*]i) [=] c[-]CC_conj c.
Proof.
 intros. elim c. intros x y. intros.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Lemma Re_wd : ∀ c c' : C, c [=] c' → ℜ c [=] ℜ c'.
Proof.
 intros c c'. elim c. intros x y. elim c'. intros x' y'.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. intros. elim H. auto.
Qed.

Lemma Im_wd : ∀ c c' : C, c [=] c' → ℑ c [=] ℑ c'.
Proof.
 intros c c'. elim c. intros x y. elim c'. intros x' y'.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. intros. elim H. auto.
Qed.

Lemma Re_resp_plus : ∀ x y : C, ℜ (x[+]y) [=] ℜ x[+]ℜ y.
Proof.
 intros. elim x. intros x1 x2. elim y. intros y1 y2.
 simpl in |- ×. unfold cc_eq in |- ×. algebra.
Qed.

Lemma Re_resp_inv : ∀ x y : C, ℜ (x[-]y) [=] ℜ x[-]ℜ y.
Proof.
 intros. elim x. intros x1 x2. elim y. intros y1 y2.
 simpl in |- ×. unfold cc_eq in |- ×. algebra.
Qed.

Lemma Im_resp_plus : ∀ x y : C, ℑ (x[+]y) [=] ℑ x[+]ℑ y.
Proof.
 intros. elim x. intros x1 x2. elim y. intros y1 y2.
 simpl in |- ×. unfold cc_eq in |- ×. algebra.
Qed.

Lemma Im_resp_inv : ∀ x y : C, ℑ (x[-]y) [=] ℑ x[-]ℑ y.
Proof.
 intros. elim x. intros x1 x2. elim y. intros y1 y2.
 simpl in |- ×. unfold cc_eq in |- ×. algebra.
Qed.

Lemma cc_calculate_square : ∀ x y, (x[+I*]y) [^]2 [=] (x[^]2[-]y[^]2) [+I*]x[*]y[*]Two.
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

End I_properties.

Hint Resolve I_square I_square' I_recip_lft I_recip_rht mult_I calculate_norm
  cc_calculate_square: algebra.
Hint Resolve I_wd Re_wd Im_wd: algebra_c.

Section Conj_properties.

Lemma CC_conj_plus : ∀ c c' : C, CC_conj (c[+]c') [=] CC_conj c[+]CC_conj c'.
Proof.
 intros c c'. elim c. intros x y. elim c'. intros x' y'.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Lemma CC_conj_mult : ∀ c c' : C, CC_conj (c[*]c') [=] CC_conj c[*]CC_conj c'.
Proof.
 intros c c'. elim c. intros x y. elim c'. intros x' y'.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Hint Resolve CC_conj_mult: algebra.

Lemma CC_conj_strext : ∀ c c' : C, CC_conj c [#] CC_conj c' → c [#] c'.
Proof.
 intros c c'. elim c. intros x y. elim c'. intros x' y'.
 simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×. intros H.
 elim H; clear H; intros.
  left. auto.
  right. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto.
Qed.

Lemma CC_conj_conj : ∀ c : C, CC_conj (CC_conj c) [=] c.
Proof.
 intros. elim c. intros x y. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Lemma CC_conj_zero : CC_conj [0] [=] [0].
Proof.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Lemma CC_conj_one : CC_conj [1] [=] [1].
Proof.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Hint Resolve CC_conj_one: algebra.

Lemma CC_conj_nexp : ∀ (c : C) n, CC_conj (c[^]n) [=] CC_conj c[^]n.
Proof.
 intros. induction n as [| n Hrecn]; intros.
 astepl (CC_conj [1]).
  Step_final ([1]:C).
 astepl (CC_conj (c[^]n[*]c)).
 astepl (CC_conj (c[^]n) [*]CC_conj c).
 Step_final (CC_conj c[^]n[*]CC_conj c).
Qed.

End Conj_properties.

Hint Resolve CC_conj_plus CC_conj_mult CC_conj_nexp CC_conj_conj
  CC_conj_zero: algebra.

Section cc_IR_properties.

Lemma Re_cc_IR : ∀ x : IR, ℜ (cc_IR x) [=] x.
Proof.
 intro x. simpl in |- ×. apply eq_reflexive.
Qed.

Lemma Im_cc_IR : ∀ x : IR, ℑ (cc_IR x) [=] [0].
Proof.
 intro x. simpl in |- ×. apply eq_reflexive.
Qed.

Lemma cc_IR_wd : ∀ x y : IR, x [=] y → cc_IR x [=] cc_IR y.
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Hint Resolve cc_IR_wd: algebra_c.

Lemma cc_IR_resp_ap : ∀ x y : IR, x [#] y → cc_IR x [#] cc_IR y.
Proof.
 intros. simpl in |- ×. unfold cc_ap in |- ×. simpl in |- ×. left. auto.
Qed.

Lemma cc_IR_mult : ∀ x y : IR, cc_IR x[*]cc_IR y [=] cc_IR (x[*]y).
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Hint Resolve cc_IR_mult: algebra.

Lemma cc_IR_mult_lft : ∀ x y z, (x[+I*]y) [*]cc_IR z [=] x[*]z[+I*]y[*]z.
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Lemma cc_IR_mult_rht : ∀ x y z, cc_IR z[*] (x[+I*]y) [=] z[*]x[+I*]z[*]y.
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; rational.
Qed.

Lemma cc_IR_plus : ∀ x y : IR, cc_IR x[+]cc_IR y [=] cc_IR (x[+]y).
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Hint Resolve cc_IR_plus: algebra.

Lemma cc_IR_minus : ∀ x y : IR, cc_IR x[-]cc_IR y [=] cc_IR (x[-]y).
Proof.
 intros. simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Lemma cc_IR_zero : cc_IR [0] [=] [0].
Proof.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Hint Resolve cc_IR_zero: algebra.

Lemma cc_IR_one : cc_IR [1] [=] [1].
Proof.
 simpl in |- ×. unfold cc_eq in |- ×. simpl in |- ×. split; algebra.
Qed.

Hint Resolve cc_IR_one: algebra.

Lemma cc_IR_nring : ∀ n : nat, cc_IR (nring n) [=] nring n.
Proof.
 intros. induction n as [| n Hrecn]; intros.
 astepl (cc_IR [0]).
  Step_final ([0]:C).
 astepl (cc_IR (nring n[+][1])).
 astepl (cc_IR (nring n) [+]cc_IR [1]).
 Step_final (nring n[+] ([1]:C)).
Qed.

Lemma cc_IR_nexp : ∀ (x : IR) (n : nat), cc_IR x[^]n [=] cc_IR (x[^]n).
Proof.
 intros. induction n as [| n Hrecn]; intros.
 astepl ([1]:C).
  Step_final (cc_IR [1]).
 astepl (cc_IR x[^]n[*]cc_IR x).
 astepl (cc_IR (x[^]n) [*]cc_IR x).
 Step_final (cc_IR (x[^]n[*]x)).
Qed.

End cc_IR_properties.

Hint Resolve Re_cc_IR Im_cc_IR: algebra.
Hint Resolve cc_IR_wd: algebra_c.
Hint Resolve cc_IR_mult cc_IR_nexp cc_IR_mult_lft cc_IR_mult_rht cc_IR_plus
  cc_IR_minus: algebra.
Hint Resolve cc_IR_nring cc_IR_zero: algebra.

Load "Transparent_algebra".
Lemma char0_CC : Char0 C.
Proof.
 unfold Char0 in |- ×.
 intros.
 astepl (cc_IR (nring n)).
 simpl in |- ×.
 unfold cc_ap in |- ×.
 simpl in |- ×.
 left.
 apply char0_IR.
 auto.
Qed.
Load "Opaque_algebra".

Lemma poly_apzero_CC : ∀ f : C[X], f [#] [0] → {c : C | f ! c [#] [0]}.
Proof.
 intros.
 apply poly_apzero.
  exact char0_CC.
 auto.
Qed.

Lemma poly_CC_extensional : ∀ p q : C[X], (∀ x, p ! x [=] q ! x) → p [=] q.
Proof.
 intros.
 apply poly_extensional.
  exact char0_CC.
 auto.
Qed.