proposition: Lemma orthogonale_segment_milieu_mediatrice : forall A B M N : PO, A <> B :>PO -> M = milieu A B :>PO -> orthogonal (vec A B) (vec M N) -> mediatrice A B N.
proof: Proof. unfold mediatrice in |- *; intros. apply carre_egalite_distance. repeat rewrite <- carre_scalaire_distance. generalize (rectangle_Pythagore M N A); unfold iff in |- *; intros. generalize (rectangle_Pythagore M N B); unfold iff in |- *; intros. elim H2; [ intros H4 H7; try clear H2 ]. elim H3; [ intros H5 H6; try clear H3 ]. cut (orthogonal (vec M N) (vec M A)); intros. rewrite H4; auto. rewrite H5. replace (scalaire (vec M A) (vec M A)) with (scalaire (vec A M) (vec A M)). rewrite (milieu_vecteur H0); auto. replace (vec M A) with (mult_PP (-1) (vec A M)). Simplscal. Ringvec. rewrite <- (milieu_vecteur H0); auto. auto with geo. apply ortho_sym. replace (vec M A) with (mult_PP (- / 2) (vec A B)). auto with geo. replace (vec M A) with (mult_PP (-1) (mult_PP (/ 2) (vec A B))). cut (2 <> 0); intros; auto with real. Fieldvec 2. rewrite <- (milieu_vecteur2 H0); auto. Ringvec. Qed.