proposition: Lemma mediatrices_reflexion : forall A B M M' : PO, M <> M' -> ~ alignes A B M -> mediatrice M M' A -> mediatrice M M' B -> M' = reflexion A B M.
proof: Proof. intros A B M M' H0 H1 H2 H3; try assumption. cut (A <> B); intros H; [ idtac | auto with geo ]. soit_milieu M M' K. apply reflexion_def2 with K; auto with geo. apply def_projete_orthogonal; auto. discrimine K A. apply alignes_ordre_cycle; auto. apply mediatrice_droite with (2 := H4); auto. cut (orthogonal (vec M M') (vec A B)); intros. apply ortho_sym. replace (vec K M) with (mult_PP (-1) (vec M K)). rewrite (milieu_vecteur2 (A:=M) (B:=M') (M:=K)); auto. replace (mult_PP (-1) (mult_PP (/ 2) (vec M M'))) with (mult_PP (- / 2) (vec M M')). Simplortho. cut (2 <> 0); intros; auto with real. Fieldvec 2. Ringvec. apply ortho_sym. apply mediatrice_orthogonale_segment; auto. Qed.