proposition: Lemma existence_point_fixe_complexe : forall (a b : C) (f : C -> C), a <> oneC -> (forall z : C, f z = Cplus (Cmult a z) b) -> exists j : C, f j = j.
proof: Proof. intros. elim existence_solution_equation with (a := a) (b := b); [ intros z0 H1; try clear existence_solution_equation; try exact H1 | auto ]. exists z0. rewrite (H0 z0). rewrite <- H1; auto. Qed.