proposition: Lemma reflexion_image_distinct : forall A B M M' : PO, ~ alignes A B M -> M' = reflexion A B M -> M <> M'.
proof: Proof. intros A B M M' H0 H1; try assumption. cut (A <> B); intros H2; [ idtac | auto with geo ]. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H3; try clear existence_projete_orthogonal; try exact H3 | auto ]. 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. cut (M <> H); intros. apply dist_non_nulle. unfold not in |- *; intros; apply H6. apply distance_nulle. rewrite (milieu_vecteur2 (A:=M) (B:=M') (M:=H)); auto. Simplscal. rewrite carre_scalaire_distance; rewrite H7; ring. unfold not in |- *; intros; apply H0. rewrite H6. elim def_projete_orthogonal2 with (A := A) (B := B) (C := M) (H := H); [ intros; try exact H7 | auto | auto ]. Qed.