proposition: Lemma mediatrice_orthogonale_segment : forall A B M N : PO, A <> B :>PO -> mediatrice A B M -> mediatrice A B N -> orthogonal (vec M N) (vec A B).
proof: Proof. intros. discrimine M N. VReplace (vec N N) zero. auto with geo. elim (classic (milieu A B = M)); intros. rewrite <- H3; rewrite <- H3 in H0. apply ortho_sym. apply mediatrice_orthogonale_segment_milieu; auto. rewrite H3; auto. elim (classic (milieu A B = N)); intros. rewrite <- H4; rewrite <- H4 in H2. replace (vec M (milieu A B)) with (add_PP (mult_PP 0 (vec (milieu A B) M)) (mult_PP (-1) (vec (milieu A B) M))). apply ortho_combinaison_lineaire; auto. apply ortho_sym; apply mediatrice_orthogonale_segment_milieu; auto. apply ortho_sym; apply mediatrice_orthogonale_segment_milieu; auto. Ringvec. cut (orthogonal (vec (milieu A B) N) (vec A B)); intros. cut (orthogonal (vec (milieu A B) M) (vec A B)); intros. replace (vec M N) with (add_PP (mult_PP 1 (vec (milieu A B) N)) (mult_PP (-1) (vec (milieu A B) M))). apply ortho_combinaison_lineaire; auto with geo. Ringvec. apply ortho_sym; apply mediatrice_orthogonale_segment_milieu; auto with geo. apply ortho_sym; apply mediatrice_orthogonale_segment_milieu; auto with geo. Qed.