proposition: Lemma egalite_point_image : forall (z z' : C) (M M' : PO), z = affixe M -> z' = affixe M' -> M = M' -> z = z'.
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z); intros a H2; elim H2; intros b H3; try clear H2; try exact H3. elim existence_parties_relles_imaginaires with (z := z'); intros a' H2; elim H2; intros b' H4; try clear H2; try exact H4. generalize (complexe_cart_point (z:=z) (a:=a) (b:=b)); intros H2. cut (vec O M = add_PP (mult_PP a (vec O I)) (mult_PP b (vec O J))); intros; auto. cut (vec O M = add_PP (mult_PP a' (vec O I)) (mult_PP b' (vec O J))); intros. elim unicite_composantes_vecteur with (a1 := a) (a2 := b) (b1 := a') (b2 := b') (O := O) (I := I) (J := J) (A := O) (B := M); [ intros H7 H8; try clear unicite_composantes_vecteur; try exact H8 | auto with geo | auto | auto ]. rewrite H3; rewrite H4; rewrite H7; rewrite H8; auto. rewrite H1. apply complexe_cart_point with z'; auto. Qed.