proposition: Lemma egalite_affixe : forall z z' : C, image z = image z' -> z = z'.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H0; try exact H0. elim existence_image_complexe with (z := z'); intros M'; intros. apply egalite_point_image with (M := M) (M' := M'); auto with geo. rewrite H0; rewrite H1; auto. Qed.