proposition: Lemma reflexion_mediatrice : forall A B M M' : PO, ~ alignes A B M -> M' = reflexion A B M -> mediatrice M M' A /\ mediatrice M M' B.
proof: Proof. intros A B M M' H1 H3; try assumption. cut (A <> B); intros H0; [ idtac | auto with geo ]. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H2; try clear existence_projete_orthogonal | auto ]. generalize (reflexion_image_distinct (A:=A) (B:=B) (M:=M) (M':=M')); intros H5. generalize (reflexion_projete_orthogonal_milieu (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros. generalize (reflexion_def (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros. elim def_projete_orthogonal2 with (A := A) (B := B) (C := M) (H := H); [ intros | auto | auto ]. halignes H7 k. split; [ try assumption | idtac ]. elim (classic (H = A)); intros. rewrite <- H10. apply milieu_mediatrice; auto. apply orthogonale_segment_milieu_mediatrice with H; auto. apply ortho_sym. cut (orthogonal (vec A B) (vec M M')); intros. replace (vec H A) with (mult_PP (- k) (vec A B)). Simplortho. replace (vec H A) with (mult_PP (-1) (vec A H)). rewrite H9. Ringvec. Ringvec. apply ortho_sym. rewrite H6; auto. Simplortho. elim (classic (H = B)); intros. rewrite <- H10. apply milieu_mediatrice; auto. apply orthogonale_segment_milieu_mediatrice with H; auto. apply ortho_sym. cut (orthogonal (vec A B) (vec M M')); intros. replace (vec H B) with (add_PP (mult_PP (- k) (vec A B)) (mult_PP 1 (vec A B))). Simplortho. replace (mult_PP (- k) (vec A B)) with (mult_PP (-1) (mult_PP k (vec A B))). rewrite <- H9. Ringvec. Ringvec. apply ortho_sym. rewrite H6; auto. Simplortho. Qed.