proposition: Lemma nrCC4_a7 : z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] [0].
proof: Proof. unfold z in |- *. unfold nrCC4_z in |- *. apply eq_transitive_unfolded with ((x[+I*]y) [^]n[*]CC_conj c[-] (x[+I*][--]y) [^]n[*]c). apply eq_reflexive_unfolded. unfold x in |- *. unfold nrCC4_x in |- *. cut ((y[*]r[+I*]y) [^]n[*]CC_conj c [=] cc_IR y[^]n[*] ((r[+I*][1]) [^]n[*]CC_conj c)). intro. cut ((y[*]r[+I*][--]y) [^]n[*]c [=] cc_IR y[^]n[*] ((r[+I*][--][1]) [^]n[*]c)). intro. apply eq_transitive_unfolded with (cc_IR y[^]n[*] ((r[+I*][1]) [^]n[*]CC_conj c) [-] cc_IR y[^]n[*] ((r[+I*][--][1]) [^]n[*]c)). apply cg_minus_wd. exact H. exact H0. apply eq_transitive_unfolded with (cc_IR y[^]n[*] ((r[+I*][1]) [^]n[*]CC_conj c[-] (r[+I*][--][1]) [^]n[*]c)). apply eq_symmetric_unfolded. apply dist_2a. apply eq_transitive_unfolded with (cc_IR y[^]n[*][0]). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. exact r_property. apply cring_mult_zero. cut ((y[*]r[+I*][--]y) [^]n [=] cc_IR y[^]n[*] (r[+I*][--][1]) [^]n). intro. apply eq_transitive_unfolded with (cc_IR y[^]n[*] (r[+I*][--][1]) [^]n[*]c). apply bin_op_wd_unfolded. exact H0. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply mult_assoc_unfolded. cut (y[*]r[+I*][--]y [=] cc_IR y[*] (r[+I*][--][1])). intro. apply eq_transitive_unfolded with ((cc_IR y[*] (r[+I*][--][1])) [^]n). apply un_op_wd_unfolded. exact H0. apply mult_nexp. cut ( [--]y [=] y[*][--][1]). intro. apply eq_transitive_unfolded with (y[*]r[+I*]y[*][--][1]). apply I_wd. apply eq_reflexive_unfolded. exact H0. apply eq_symmetric_unfolded. apply cc_IR_mult_rht. apply eq_transitive_unfolded with ( [--] (y[*][1])). apply un_op_wd_unfolded. apply eq_symmetric_unfolded. apply mult_one. apply eq_symmetric_unfolded. apply cring_inv_mult_lft. cut ((y[*]r[+I*]y) [^]n [=] cc_IR y[^]n[*] (r[+I*][1]) [^]n). intro. apply eq_transitive_unfolded with (cc_IR y[^]n[*] (r[+I*][1]) [^]n[*]CC_conj c). apply bin_op_wd_unfolded. exact H. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply mult_assoc_unfolded. cut (y[*]r[+I*]y [=] cc_IR y[*] (r[+I*][1])). intro. apply eq_transitive_unfolded with ((cc_IR y[*] (r[+I*][1])) [^]n). apply un_op_wd_unfolded. exact H. apply mult_nexp. apply eq_transitive_unfolded with (y[*]r[+I*]y[*][1]). apply I_wd. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply mult_one. apply eq_symmetric_unfolded. apply cc_IR_mult_rht. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing