proposition: Lemma mediatrice_distinct_extremite : forall A B M : PO, A <> B -> mediatrice A B M -> M <> A /\ M <> B.
proof: Proof. unfold mediatrice in |- *; intros. cut (~ (M = A \/ M = B)); intros. intuition. unfold not in |- *; intros; apply H. elim H1; [ intros H2; try clear H1; rewrite <- H2; rewrite <- H2 in H0 | intros H2; try clear H1; rewrite <- H2; rewrite <- H2 in H0 ]. apply distance_nulle; auto. rewrite carre_scalaire_distance; rewrite <- H0; rewrite <- carre_scalaire_distance. replace (vec M M) with (mult_PP 0 (vec A B)). Simplscal. Ringvec. apply distance_nulle. replace (vec A M) with (mult_PP (-1) (vec M A)). Simplscal. rewrite carre_scalaire_distance; rewrite H0; rewrite <- carre_scalaire_distance. replace (vec M M) with (mult_PP 0 (vec A B)). Simplscal. Ringvec. Ringvec. Qed.