proposition: Lemma equation_solution : forall z z' j : C, z' = f z -> f j = j -> Cplus z' (Copp j) = Cmult a (Cplus z (Copp j)).
proof: Proof. intros z z' j; try assumption. repeat rewrite f_def; intros. rewrite H. pattern j at 1 in |- *. rewrite <- H0; ring. Qed.