proposition: Lemma projete_orthogonal_image : forall A B M M' H : PO, A <> B -> H = projete_orthogonal A B M -> M' = reflexion A B M -> H = projete_orthogonal A B M'.
proof: Proof. intros. generalize (reflexion_def (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros H5. generalize (reflexion_projete_orthogonal_milieu (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 ]. apply def_projete_orthogonal; auto. apply ortho_sym. replace (vec H M') with (vec M H); auto with geo. Qed.