proposition: Lemma nrCC3_a1 : forall p r, (Im_poly p) ! r [=] Im p ! (cc_IR r).
proof: Proof. intros. elim p; intros. unfold Im_poly in |- *. apply eq_transitive_unfolded with ZeroR. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (Im ([0]:CC)); apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (cpoly_linear _ (Im s) (Im_poly c)) ! r. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (Im s[+]r[*] (Im_poly c) ! r). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (Im s[+]r[*]Im c ! (cc_IR r)). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. exact H. cut (forall (r : IR) (c : CC), r[*]Im c [=] Im (cc_IR r[*]c)); intros. apply eq_transitive_unfolded with (Im s[+]Im (cc_IR r[*]c ! (cc_IR r))). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply H0. apply eq_transitive_unfolded with (Im (s[+]cc_IR r[*]c ! (cc_IR r))). apply eq_reflexive_unfolded. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (r0[*]Im c0[+][0]). apply eq_symmetric_unfolded. apply cm_rht_unit_unfolded. apply eq_transitive_unfolded with (r0[*]Im c0[+][0][*]Re c0). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply cring_mult_zero_op. apply eq_transitive_unfolded with (Im ((r0[+I*][0]) [*] (Re c0[+I*]Im c0))). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (Im (cc_IR r0[*] (Re c0[+I*]Im c0))). apply eq_reflexive_unfolded. apply eq_reflexive_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing