proposition: Lemma affixe_image : forall z : C, affixe (image z) = z.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H; try clear existence_image_complexe; try exact H. rewrite <- H; symmetry in |- *; auto with geo. Qed.