proposition: Lemma egalite_affixe_point : forall (z z' : C) (M M' : PO), z = affixe M -> z' = affixe M' -> z = z' -> M = M'.
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. apply vecteur_nul_conf. replace (vec M M') with (add_PP (vec O M') (mult_PP (-1) (vec O M))); [ idtac | Ringvec ]. elim unicite_parties_relles_imaginaires with (z := z) (a := a) (b := b) (a' := a') (b' := b'); [ intros; try exact H8 | auto | auto ]. rewrite H5; rewrite H6; rewrite H7; rewrite H8. Ringvec. rewrite H1; auto. apply complexe_cart_point with z'; auto. Qed.