proposition: Lemma reflexion_axe_orthogonal_segment : forall A B M M' : PO, ~ alignes A B M -> M' = reflexion A B M -> orthogonal (vec M M') (vec A B).
proof: Proof. intros. assert (A <> B); auto with geo. apply ortho_sym; auto. elim (reflexion_mediatrice (A:=A) (B:=B) (M:=M) (M':=M')); auto; intros. apply mediatrice_orthogonale_segment; auto. apply reflexion_image_distinct with (2 := H0); auto. Qed.