proposition: Lemma non_axe_image_non_axe : forall A B M M' : PO, ~ alignes A B M -> M' = reflexion A B M -> ~ alignes A B M'.
proof: Proof. intros A B M M' H0 H2; try assumption. cut (A <> B); intros H1; [ 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. elim reflexion_mediatrice with (A := A) (B := B) (M := M) (M' := M'); [ intros H6 H7; try clear reflexion_mediatrice; try exact H7 | auto | auto ]. generalize (mediatrice_orthogonale_segment (A:=M) (B:=M') (M:=A) (N:=B)); intros. generalize (reflexion_image_distinct (A:=A) (B:=B) (M:=M) (M':=M')); intros. elim def_projete_orthogonal2 with (A := A) (B := B) (C := M) (H := H); [ intros | auto | auto ]. cut (H = projete_orthogonal A B M'); intros. cut (M' <> H); intros. unfold not in |- *; intros; apply H13. rewrite H12. apply def_projete_orthogonal; auto. replace (vec M' M') with zero. apply zero_ortho_tout. Ringvec. rewrite H4; auto. apply milieu_distinct2; auto. apply projete_orthogonal_image with M; auto. Qed.