proposition: Lemma imag_to_real : forall a b a' b', a'[+I*]b' [=] (a[+I*]b) [*]II -> a [#] [0] -> b' [#] [0].
proof: Proof. intros ????? H0. cut (b' [=] a); intros. now apply ap_wdl with a. apply eq_transitive with (Im (a'[+I*]b')). apply eq_reflexive. apply eq_transitive with (Im ((a[+I*]b) [*]II)). now apply Im_wd. apply eq_transitive with (Im ( [--]b[+I*]a)). apply Im_wd. apply mult_I. apply eq_reflexive. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing