CoRN.complex.CComplex
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.
Maps from reals to complex and vice-versa are defined, as well as conjugate,
absolute value and the imaginary unit I
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).
Properties of i
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.
C has characteristic zero
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.